src/HOL/Library/reflection.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 37117 59cee8807c29
--- a/src/HOL/Library/reflection.ML	Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Library/reflection.ML	Sat May 15 21:50:05 2010 +0200
@@ -133,7 +133,7 @@
                              (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds))
                in (([(ta, ctxt')],
                     fn ([th], bds) =>
-                      (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]),
+                      (hd (Variable.export ctxt' ctxt [(Thm.forall_intr (cert x) th) COMP allI]),
                        let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT))
                        in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
                        end)),