Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/atomize_elim.ML
changeset 41228 e1fce873b814
parent 35625 9c818cab0dd0
child 42083 e1209fc7ecdc 
--- a/src/Tools/atomize_elim.ML	Fri Dec 17 16:25:21 2010 +0100
+++ b/src/Tools/atomize_elim.ML	Fri Dec 17 17:08:56 2010 +0100
@@ -60,7 +60,7 @@
 *)
 fun atomize_elim_conv ctxt ct =
     (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
-    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
+    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
     then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))
isabelle