changeset 59621 | 291934bac95e |
parent 59582 | 0fbed69ff081 |
child 59875 | 9779b0c59ad4 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Mar 06 15:58:56 2015 +0100 @@ -807,7 +807,7 @@ | freeze (Free (s, T)) = Free (s, freezeT T) | freeze t = t -fun goal_of_thm thy = Thm.prop_of #> freeze #> Thm.cterm_of thy #> Goal.init +fun goal_of_thm thy = Thm.prop_of #> freeze #> Thm.global_cterm_of thy #> Goal.init fun run_prover_for_mash ctxt params prover goal_name facts goal = let