# HG changeset patch # User wenzelm # Date 1206470397 -3600 # Node ID 6e8aa5a4eb82200e200b6bdb1de5dad1ff672c7d # Parent 99d4cbb1f941fb37b15a978c88bcacacddf9e309 more antiquotations; diff -r 99d4cbb1f941 -r 6e8aa5a4eb82 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Tue Mar 25 12:14:17 2008 +0100 +++ b/src/CCL/Wfd.thy Tue Mar 25 19:39:57 2008 +0100 @@ -539,8 +539,8 @@ apply (unfold let_def) apply (rule 1 [THEN canonical]) apply (tactic {* - REPEAT (DEPTH_SOLVE_1 (resolve_tac (thms "prems" @ thms "eval_rls") 1 ORELSE - etac (thm "substitute") 1)) *}) + REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE + etac @{thm substitute} 1)) *}) done lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c" diff -r 99d4cbb1f941 -r 6e8aa5a4eb82 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Tue Mar 25 12:14:17 2008 +0100 +++ b/src/CTT/CTT.thy Tue Mar 25 19:39:57 2008 +0100 @@ -500,7 +500,7 @@ apply (unfold basic_defs) apply (rule major [THEN SumE]) apply (rule SumC [THEN subst_eqtyparg, THEN replace_type]) - apply (tactic {* typechk_tac (thms "prems") *}) + apply (tactic {* typechk_tac @{thms assms} *}) done end