src/CTT/CTT.thy
changeset 26391 6e8aa5a4eb82
parent 23467 d1b97708d5eb
child 26956 1309a6a0a29f
     1.1 --- a/src/CTT/CTT.thy	Tue Mar 25 12:14:17 2008 +0100
     1.2 +++ b/src/CTT/CTT.thy	Tue Mar 25 19:39:57 2008 +0100
     1.3 @@ -500,7 +500,7 @@
     1.4    apply (unfold basic_defs)
     1.5    apply (rule major [THEN SumE])
     1.6    apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
     1.7 -  apply (tactic {* typechk_tac (thms "prems") *})
     1.8 +  apply (tactic {* typechk_tac @{thms assms} *})
     1.9    done
    1.10  
    1.11  end