changeset 59621 | 291934bac95e |
parent 59616 | eb59c6968219 |
child 59623 | 920889b0788e |
--- a/src/Pure/variable.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/Pure/variable.ML Fri Mar 06 15:58:56 2015 +0100 @@ -589,7 +589,7 @@ let val thy = Thm.theory_of_cterm goal; val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt; - val ps' = map (Thm.cterm_of thy o Free) ps; + val ps' = map (Thm.global_cterm_of thy o Free) ps; val goal' = fold forall_elim_prop ps' goal; in ((xs ~~ ps', goal'), ctxt') end;