diff --git a/collects/macro-debugger/model/deriv-c.ss b/collects/macro-debugger/model/deriv-c.ss
index 7260748..3efb19f 100644
--- a/collects/macro-debugger/model/deriv-c.ss
+++ b/collects/macro-debugger/model/deriv-c.ss
@@ -89,6 +89,9 @@
   (srenames sbindrhss vrenames vrhss body tag)
   #:transparent)
 
+;;   (make-p:provide <Base> (listof Deriv) ?exn)
+(define-struct (p:provide prule) (inners ?2) #:transparent)
+
 ;;   (make-p:stop <Base>)
 ;;   (make-p:unknown <Base>)
 ;;   (make-p:#%top <Base> Stx)
@@ -98,7 +101,6 @@
 ;;   (make-p:require <Base>)
 ;;   (make-p:require-for-syntax <Base>)
 ;;   (make-p:require-for-template <Base>)
-;;   (make-p:provide <Base>)
 ;;   (make-p:#%variable-reference <Base>)
 (define-struct (p::STOP prule) () #:transparent)
 (define-struct (p:stop p::STOP) () #:transparent)
@@ -110,7 +112,6 @@
 (define-struct (p:require p::STOP) () #:transparent)
 (define-struct (p:require-for-syntax p::STOP) () #:transparent)
 (define-struct (p:require-for-template p::STOP) () #:transparent)
-(define-struct (p:provide p::STOP) () #:transparent)
 (define-struct (p:#%variable-reference p::STOP) () #:transparent)
 
 ;; A LDeriv is
diff --git a/collects/macro-debugger/model/deriv-parser.ss b/collects/macro-debugger/model/deriv-parser.ss
index cbe0417..029041c 100644
--- a/collects/macro-debugger/model/deriv-parser.ss
+++ b/collects/macro-debugger/model/deriv-parser.ss
@@ -288,8 +288,8 @@
      [()
       (make mod:skip)]
      ;; provide: special
-     [(enter-prim prim-provide (? ModuleProvide/Inner) exit-prim)
-      (make mod:cons (make p:provide $1 $4 null $3))]
+     [(enter-prim prim-provide (? ModuleProvide/Inner) ! exit-prim)
+      (make mod:cons (make p:provide $1 $5 null #f $3 $4))]
      ;; normal: expand completely
      [((? EE))
       (make mod:cons $1)]
@@ -298,10 +298,10 @@
       (make mod:lift $1 #f $2)])
 
     (ModuleProvide/Inner
-     [() #f]
-     [(!!) $1]
+     (#:skipped null)
+     [() null]
      [((? EE) (? ModuleProvide/Inner))
-      $2])
+      (cons $1 $2)])
 
     ;; Definitions
     (PrimDefineSyntaxes
@@ -442,7 +442,7 @@
 
     (PrimProvide 
      (#:args e1 e2 rs)
-     [(prim-provide !) (make p:provide e1 e2 rs $2)])
+     [(prim-provide !) (make p:provide e1 e2 rs $2 null #f)])
 
     (PrimVarRef
      (#:args e1 e2 rs)
diff --git a/collects/macro-debugger/model/reductions.ss b/collects/macro-debugger/model/reductions.ss
index 67671a7..8ded0fb 100644
--- a/collects/macro-debugger/model/reductions.ss
+++ b/collects/macro-debugger/model/reductions.ss
@@ -194,9 +194,23 @@
         [#:pattern (?top . ?var)]
         [#:learn (list #'?var)])]
 
-    [(Wrap p:provide (e1 e2 rs ?1))
-     (R [! ?1]
-        [#:walk e2 'provide])]
+    [(Wrap p:provide (e1 e2 rs ?1 inners ?2))
+     (let ([wrapped-inners
+            (for/list ([inner inners])
+              (match inner
+                [(Wrap deriv (e1 e2))
+                 (make local-expansion e1 e2
+                       #f e1 inner #f e2 #f)]))])
+       (R [! ?1]
+          [#:pattern ?form]
+          [#:pass1]
+          [#:left-foot]
+          [LocalActions ?form wrapped-inners]
+          [! ?2]
+          [#:pass2]
+          [#:set-syntax e2]
+          [#:step 'provide]
+          [#:set-syntax e2]))]
 
     [(Wrap p:stop (e1 e2 rs ?1))
      (R [! ?1])]