# 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