--- 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;