--- a/src/HOL/Tools/induct_method.ML Fri Dec 22 18:23:41 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML Fri Dec 22 18:24:11 2000 +0100
@@ -10,6 +10,7 @@
sig
val vars_of: term -> term list
val concls_of: thm -> term list
+ val rewrite_cterm: thm list -> cterm -> cterm
val simp_case_tac: bool -> simpset -> int -> tactic
val setup: (theory -> theory) list
end;
@@ -72,6 +73,9 @@
|> mapfilter prep_var
end;
+fun rewrite_cterm rews =
+ #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
+
(* simplifying cases rules *)
@@ -200,9 +204,6 @@
local
-fun rewrite_cterm rews =
- #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
-
fun drop_Trueprop ct =
let
fun drop (Abs (x, T, t)) = Abs (x, T, drop t)