# HG changeset patch
# User berghofe
# Date 1022863771 -7200
# Node ID 0567f4fd1415fcfbe33ea85c9fc61fd3ae3340ab
# Parent  08c42252346f80b0663ae2317faf5e571065e227
Changed interface of MetaSimplifier.rewrite_term.

diff -r 08c42252346f -r 0567f4fd1415 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri May 31 18:48:31 2002 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri May 31 18:49:31 2002 +0200
@@ -294,7 +294,7 @@
 val all_not_allowed = 
     "Introduction rule must not have a leading \"!!\" quantifier";
 
-fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize;
+fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize [];
 
 in
 
diff -r 08c42252346f -r 0567f4fd1415 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Fri May 31 18:48:31 2002 +0200
+++ b/src/Provers/induct_method.ML	Fri May 31 18:49:31 2002 +0200
@@ -136,13 +136,13 @@
 (* atomize and rulify *)
 
 fun atomize_term sg =
-  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize;
+  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize [];
 
 fun rulified_term thm =
   let val sg = Thm.sign_of_thm thm in
     Thm.prop_of thm
-    |> MetaSimplifier.rewrite_term sg Data.rulify1
-    |> MetaSimplifier.rewrite_term sg Data.rulify2
+    |> MetaSimplifier.rewrite_term sg Data.rulify1 []
+    |> MetaSimplifier.rewrite_term sg Data.rulify2 []
     |> pair sg
   end;
 
diff -r 08c42252346f -r 0567f4fd1415 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Fri May 31 18:48:31 2002 +0200
+++ b/src/Pure/Isar/object_logic.ML	Fri May 31 18:49:31 2002 +0200
@@ -129,7 +129,7 @@
       (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));
 
 fun atomize_term sg =
-  drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg);
+  drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) [];
 
 fun atomize_tac i st =
   if Logic.has_meta_prems (Thm.prop_of st) i then