--- a/QuotMain.thy	Wed Oct 14 09:47:16 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 09:50:13 2009 +0200
@@ -418,24 +418,18 @@
 *}
 
 
-term Respects
-
 ML {*
-fun atomize_thm t =
-  MetaSimplifier.rewrite_rule [ObjectLogic.atomize (cterm_of @{theory} (prop_of t))] t
+fun atomize_thm thm =
+let
+  val thm' = forall_intr_vars thm
+  val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+  Simplifier.rewrite_rule [thm''] thm'
+end
 *}
 
-ML {*
-fun meta_quantify t =
-  let
-    val vars = Term.add_vars (prop_of t) [];
-    val cvars = map (fn x => cterm_of @{theory} (Var x)) vars
-  in
-    fold forall_intr cvars t
-  end
-*}
-
-ML {* atomize_thm (meta_quantify @{thm list.induct}) *}
+thm list.induct
+ML {* atomize_thm @{thm list.induct} *}
 
 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
   trm == new_trm
@@ -1119,7 +1113,7 @@
 
 thm list.induct
 
-ML {* val li = Thm.freezeT (atomize_thm (meta_quantify @{thm list.induct})) *}
+ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
 ML {*
 Syntax.string_of_term @{context}  (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
@@ -1181,7 +1175,7 @@
   fun lift_theorem_fset name thm lthy =
     let
       val lifted_thm = lift_theorem_fset_aux thm lthy;
-      val (_, lthy2) = note_thm (name, lifted_thm) lthy;
+      val (_, lthy2) = note (name, lifted_thm) lthy;
     in
       lthy2
     end;