# HG changeset patch
# User wenzelm
# Date 1192969313 -7200
# Node ID dffe405b090deb3c2bc9d334b8e9c980068e6e56
# Parent  2c8caac48adeb57f76400617a51174b5f1bf90d8
removed obsolete ML bindings;

diff -r 2c8caac48ade -r dffe405b090d src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Oct 21 14:21:48 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Oct 21 14:21:53 2007 +0200
@@ -316,14 +316,14 @@
 
   fun pat_strict c =
     let
-      val axs = branch_def :: axs_pat_def;
+      val axs = @{thm branch_def} :: axs_pat_def;
       val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
       val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
     in pg axs goal tacs end;
 
   fun pat_app c (con, args) =
     let
-      val axs = branch_def :: axs_pat_def;
+      val axs = @{thm branch_def} :: axs_pat_def;
       val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
       val rhs = if con = fst c then pat_rhs c else %%:failN;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
diff -r 2c8caac48ade -r dffe405b090d src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Sun Oct 21 14:21:48 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Oct 21 14:21:53 2007 +0200
@@ -98,7 +98,7 @@
     val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
     val (fixdef_thms, thy') =
       PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
-    val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
+    val ctuple_fixdef_thm = foldr1 (fn (x,y) => @{thm cpair_equalI} OF [x,y]) fixdef_thms;
     
     val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
     val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
@@ -110,8 +110,8 @@
     fun unfolds [] thm = []
       | unfolds (n::[]) thm = [(n^"_unfold", thm)]
       | unfolds (n::ns) thm = let
-          val thmL = thm RS cpair_eqD1;
-          val thmR = thm RS cpair_eqD2;
+          val thmL = thm RS @{thm cpair_eqD1};
+          val thmR = thm RS @{thm cpair_eqD2};
         in (n^"_unfold", thmL) :: unfolds ns thmR end;
     val unfold_thms = unfolds names ctuple_unfold_thm;
     val thms = ctuple_induct_thm :: unfold_thms;
@@ -210,7 +210,7 @@
 (* proves a block of pattern matching equations as theorems, using unfold *)
 fun make_simps thy (unfold_thm, eqns) =
   let
-    val tacs = [rtac (unfold_thm RS ssubst_lhs) 1, asm_simp_tac (simpset_of thy) 1];
+    val tacs = [rtac (unfold_thm RS @{thm ssubst_lhs}) 1, asm_simp_tac (simpset_of thy) 1];
     fun prove_term t = Goal.prove_global thy [] [] t (K (EVERY tacs));
     fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
   in