src/CTT/rew.ML
changeset 19761 5cd82054c2c6
parent 17496 26535df536ae
child 35762 af3ff2ba4c54
--- a/src/CTT/rew.ML	Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/rew.ML	Fri Jun 02 18:15:38 2006 +0200
@@ -1,15 +1,15 @@
-(*  Title:      CTT/rew
+(*  Title:      CTT/rew.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Simplifier for CTT, using Typedsimp
+Simplifier for CTT, using Typedsimp.
 *)
 
 (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
   for using assumptions as rewrite rules*)
 fun peEs 0 = []
-  | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
+  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
 
 (*Tactic used for proving conditions for the cond_rls*)
 val prove_cond_tac = eresolve_tac (peEs 5);
@@ -17,19 +17,19 @@
 
 structure TSimp_data: TSIMP_DATA =
   struct
-  val refl              = refl_elem
-  val sym               = sym_elem
-  val trans             = trans_elem
-  val refl_red          = refl_red
-  val trans_red         = trans_red
-  val red_if_equal      = red_if_equal
-  val default_rls       = comp_rls
-  val routine_tac       = routine_tac routine_rls
+  val refl              = thm "refl_elem"
+  val sym               = thm "sym_elem"
+  val trans             = thm "trans_elem"
+  val refl_red          = thm "refl_red"
+  val trans_red         = thm "trans_red"
+  val red_if_equal      = thm "red_if_equal"
+  val default_rls       = thms "comp_rls"
+  val routine_tac       = routine_tac (thms "routine_rls")
   end;
 
 structure TSimp = TSimpFun (TSimp_data);
 
-val standard_congr_rls = intrL2_rls @ elimL_rls;
+val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
 
 (*Make a rewriting tactic from a normalization tactic*)
 fun make_rew_tac ntac =