src/Pure/old_goals.ML
changeset 26653 60e0cf6bef89
parent 26626 c6231d64d264
child 26665 2e363edf7578
     1.1 --- a/src/Pure/old_goals.ML	Tue Apr 15 16:12:01 2008 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Tue Apr 15 16:12:05 2008 +0200
     1.3 @@ -159,7 +159,7 @@
     1.4              forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As;
     1.5        val (As,B) = if atoms then ([],horn) else (As,B);
     1.6        val cAs = map (cterm_of thy) As;
     1.7 -      val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
     1.8 +      val prems = map (rewrite_rule rths o Thm.forall_elim_vars 0 o Thm.assume) cAs;
     1.9        val cB = cterm_of thy B;
    1.10        val st0 = let val st = Goal.init cB |> fold Thm.weaken cAs
    1.11                  in  rewrite_goals_rule rths st end