# HG changeset patch
# User wenzelm
# Date 977505851 -3600
# Node ID 13cb6d29f7ff94cb38d96012ef7f06fe39dcd238
# Parent  2ccafccb81c05ff46264a74e36a2db9c1ff75ece
export rewrite_cterm;

diff -r 2ccafccb81c0 -r 13cb6d29f7ff src/HOL/Tools/induct_method.ML
--- 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)