--- a/QuotMain.thy	Tue Dec 01 12:16:45 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 14:04:00 2009 +0100
@@ -260,49 +260,6 @@
 *}
 
 
-section {*  Infrastructure about definitions *}
-
-(* Does the same as 'subst' in a given theorem *)
-ML {*
-fun eqsubst_thm ctxt thms thm =
-  let
-    val goalstate = Goal.init (Thm.cprop_of thm)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      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 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 equal_elim_rule1} OF [rt, thm]
-  end
-*}
-
-(* expects atomized definitions *)
-ML {*
-fun add_lower_defs_aux lthy thm =
-  let
-    val e1 = @{thm fun_cong} OF [thm];
-    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
-    val g = simp_ids f
-  in
-    (simp_ids thm) :: (add_lower_defs_aux lthy g)
-  end
-  handle _ => [simp_ids thm]
-*}
-
-ML {*
-fun add_lower_defs lthy def =
-  let
-    val def_pre_sym = symmetric def
-    val def_atom = atomize_thm def_pre_sym
-    val defs_all = add_lower_defs_aux lthy def_atom
-  in
-    map Thm.varifyT defs_all
-  end
-*}
-
 section {* Infrastructure for collecting theorems for starting the lifting *}
 
 ML {*
@@ -402,9 +359,9 @@
 *}
 
 ML {*
-val mk_babs = Const (@{const_name "Babs"}, dummyT)
-val mk_ball = Const (@{const_name "Ball"}, dummyT)
-val mk_bex  = Const (@{const_name "Bex"}, dummyT)
+val mk_babs = Const (@{const_name Babs}, dummyT)
+val mk_ball = Const (@{const_name Ball}, dummyT)
+val mk_bex  = Const (@{const_name Bex}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 *}