# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255465335 -7200
# Node ID 19d3856abb81d1a426037b55609780566a5582b1
# Parent  9220c51e5155f5e9e20dc7eedf58d95c9a3ebfc9
slight simplification of atomize_thm

diff -r 9220c51e5155 -r 19d3856abb81 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 13 18:01:54 2009 +0200
+++ b/QuotMain.thy	Tue Oct 13 22:22:15 2009 +0200
@@ -415,24 +415,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
@@ -1116,7 +1110,7 @@
 
 thm list.induct
 
-ML {* val li = atomize_thm (meta_quantify @{thm list.induct}) *}
+ML {* val li = atomize_thm @{thm list.induct} *}
 
 ML {* (* Doesn't recognize that 'a list = '?a list *)
   cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
@@ -1171,7 +1165,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;