Changed interface of MetaSimplifier.rewrite_term.
--- 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
--- 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;
--- 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