src/Pure/drule.ML
changeset 9460 53d7ad5bec39
parent 9455 f23722b4fbe7
child 9547 8dad21f06b24
     1.1 --- a/src/Pure/drule.ML	Fri Jul 28 16:08:41 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Sun Jul 30 12:48:55 2000 +0200
     1.3 @@ -661,7 +661,7 @@
     1.4      (tag_rule internal_tag (standard (Thm.equal_elim G_def (Thm.assume G))));
     1.5  end;
     1.6  
     1.7 -val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign (Const ("Goal", propT --> propT)));
     1.8 +val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
     1.9  fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
    1.10  
    1.11