--- a/QuotMain.thy	Mon Nov 09 15:23:33 2009 +0100
+++ b/QuotMain.thy	Mon Nov 09 15:40:43 2009 +0100
@@ -441,10 +441,6 @@
 *)
 
 
-(* Needed to have a meta-equality *)
-lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
-by (simp add: id_def)
-
 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 ML {*
 fun exchange_ty lthy rty qty ty =
@@ -464,7 +460,7 @@
         Type (s, map (exchange_ty lthy rty qty) tys)
       end
   end
-  handle _ => ty (* for dest_Type *)
+  handle TYPE _ => ty (* for dest_Type *)
 *}
 
 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -472,7 +468,7 @@
 
 quotient ql = "'a list" / "Rl"
   by (rule Rl_eq)
-ML {* 
+ML {*
   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
 *}
@@ -546,7 +542,7 @@
     let val (s, tys) = dest_Type ty in
     flat (map (find_matching_types rty) tys)
     end
-    handle _ => []
+    handle TYPE _ => []
 *}
 
 ML {*
@@ -618,8 +614,9 @@
       NONE => error "eqsubst_thm"
     | SOME th => cprem_of th 1
     val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
-    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
-    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+    val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
   in
     @{thm Pure.equal_elim_rule1} OF [rt, thm]
   end
@@ -631,6 +628,10 @@
     handle _ => thm
 *}
 
+(* Needed to have a meta-equality *)
+lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
+by (simp add: id_def)
+
 ML {*
 fun build_repabs_term lthy thm consts rty qty =
   let
@@ -762,10 +763,10 @@
     val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
                  (Const (@{const_name Ball}, _) $ _)) = term_of concl
   in
-    ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
     THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-    (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
+    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
   end
   handle _ => no_tac
   )
@@ -777,10 +778,10 @@
     val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
                  (Const (@{const_name Bex}, _) $ _)) = term_of concl
   in
-    ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
     THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-    (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
+    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
   end
   handle _ => no_tac
   )
@@ -803,7 +804,7 @@
     rtac reflex_thm,
     atac,
     (
-     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
      THEN_ALL_NEW (fn _ => no_tac)
     ),
     WEAK_LAMBDA_RES_TAC ctxt,
@@ -995,7 +996,7 @@
     val rhs = mk_abs (list_comb((mk_rep f), rargs));
     val eq = Logic.mk_equals (rhs, lhs);
     val ceq = cterm_of (ProofContext.theory_of lthy') eq;
-    val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps});
+    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
     val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
     val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
   in