--- a/UnusedQuotMain.thy	Wed Nov 25 11:41:42 2009 +0100
+++ b/UnusedQuotMain.thy	Wed Nov 25 11:58:56 2009 +0100
@@ -1,3 +1,26 @@
+ML {*
+fun repeat_eqsubst_thm ctxt thms thm =
+  repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+  handle _ => thm
+*}
+
+
+ML {*
+fun eqsubst_prop ctxt thms t =
+  let
+    val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_prop"
+    | SOME th => cprem_of th 1
+  in term_of a' end
+*}
+
+ML {*
+  fun repeat_eqsubst_prop ctxt thms t =
+    repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
+    handle _ => t
+*}
+
 
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}
@@ -444,6 +467,27 @@
   end
 *}
 
+
+ML {*
+fun atomize_goal thy gl =
+  let
+    val vars = map Free (Term.add_frees gl []);
+    val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
+    fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
+    val glv = fold lambda_all vars gl
+    val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
+    val glf = Type.legacy_freeze gla
+  in
+    if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
+  end
+*}
+
+
+ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
+ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *}
+
+
+
 ML {*
 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
 let
@@ -484,3 +528,10 @@
   end
 *}
 
+ML {*
+fun simp_ids_trm trm =
+  trm |>
+  MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+  |> cprop_of |> Thm.dest_equals |> snd
+
+*}