--- a/QuotMain.thy	Mon Oct 26 11:34:02 2009 +0100
+++ b/QuotMain.thy	Mon Oct 26 11:55:36 2009 +0100
@@ -720,6 +720,31 @@
     ])
 *}
 
+ML {*
+fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+  let
+    val rt = build_repabs_term lthy thm constructors rty qty;
+    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
+    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
+      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
+    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
+  in
+    (rt, cthm, thm)
+  end
+*}
+
+ML {*
+fun repabs_eq2 lthy (rt, thm, othm) =
+  let
+    fun tac2 ctxt =
+     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
+     THEN' (rtac othm);
+    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
+  in
+    cthm
+  end
+*}
+
 section {* Cleaning the goal *}
 
 text {* Does the same as 'subst' in a given theorem *}
@@ -738,4 +763,29 @@
   end
 *}
 
+text {* expects atomized definition *}
+ML {*
+  fun add_lower_defs_aux ctxt thm =
+    let
+      val e1 = @{thm fun_cong} OF [thm]
+      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1
+    in
+      thm :: (add_lower_defs_aux ctxt f)
+    end
+    handle _ => [thm]
+*}
+
+ML {*
+fun add_lower_defs ctxt defs =
+  let
+    val defs_pre_sym = map symmetric defs
+    val defs_atom = map atomize_thm defs_pre_sym
+    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
+    val defs_sym = map (fn t => eq_reflection OF [t]) defs_all
+  in
+    map Thm.varifyT defs_sym
+  end
+*}
+
+
 end