src/HOL/Library/reflection.ML
changeset 45403 7a0b8debef77
parent 43960 c2554cc82d34
child 46510 696f3fec3f83
--- a/src/HOL/Library/reflection.ML	Tue Nov 08 08:56:24 2011 +0100
+++ b/src/HOL/Library/reflection.ML	Tue Nov 08 11:44:37 2011 +0100
@@ -60,10 +60,11 @@
    fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
      | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
    fun tryext x = (x RS ext2 handle THM _ =>  x)
-   val cong = (Goal.prove ctxt'' [] (map mk_def env)
-                          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
-                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
-                                                        THEN rtac th' 1)) RS sym
+   val cong =
+    (Goal.prove ctxt'' [] (map mk_def env)
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
+      (fn {context, prems, ...} =>
+        Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym
 
    val (cong' :: vars') =
        Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)