src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Fri Dec 17 16:25:21 2010 +0100
+++ b/src/Pure/Isar/local_defs.ML	Fri Dec 17 17:08:56 2010 +0100
@@ -182,7 +182,7 @@
 end;
 
 fun contract ctxt defs ct th =
-  trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];
+  trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)];
 
 
 (** defived definitions **)
@@ -208,8 +208,8 @@
 (* meta rewrite rules *)
 
 fun meta_rewrite_conv ctxt =
-  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
-    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
+  Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+    (Raw_Simplifier.context ctxt empty_ss
       addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
       addsimps (Rules.get (Context.Proof ctxt)));
 
@@ -220,11 +220,11 @@
 
 fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
 
-val unfold       = meta MetaSimplifier.rewrite_rule;
-val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
-val unfold_tac   = meta MetaSimplifier.rewrite_goals_tac;
-val fold         = meta MetaSimplifier.fold_rule;
-val fold_tac     = meta MetaSimplifier.fold_goals_tac;
+val unfold       = meta Raw_Simplifier.rewrite_rule;
+val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
+val unfold_tac   = meta Raw_Simplifier.rewrite_goals_tac;
+val fold         = meta Raw_Simplifier.fold_rule;
+val fold_tac     = meta Raw_Simplifier.fold_goals_tac;
 
 
 (* derived defs -- potentially within the object-logic *)
@@ -244,7 +244,7 @@
       in
         Goal.prove ctxt' frees [] prop (K (ALLGOALS
           (CONVERSION (meta_rewrite_conv ctxt') THEN'
-            MetaSimplifier.rewrite_goal_tac [def] THEN'
+            rewrite_goal_tac [def] THEN'
             resolve_tac [Drule.reflexive_thm])))
         handle ERROR msg => cat_error msg "Failed to prove definitional specification"
       end;