--- a/QuotMain.thy	Thu Nov 05 10:23:27 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 10:46:54 2009 +0100
@@ -347,8 +347,9 @@
       (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
 *}
 
-(*ML {*
-  (*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*)
+(*
+ML {*
+  text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*}
   val r = Free ("R", dummyT);
   val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
   val t2 = Syntax.check_term @{context} t;
@@ -377,7 +378,7 @@
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
   let
-    val g = build_regularize_goal thm rty rel lthy;
+    val goal = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
       (ObjectLogic.full_atomize_tac) THEN'
      REPEAT_ALL_NEW (FIRST' [
@@ -390,10 +391,11 @@
       EqSubst.eqsubst_tac ctxt [0]
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])],
-      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+      (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
      ]);
-    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
+    val cthm = Goal.prove lthy [] [] goal 
+      (fn {context,...} => tac context 1);
   in
     cthm OF [thm]
   end