src/Pure/goal.ML
changeset 28619 89f9dd800a22
parent 28446 a01de3b3fa2e
child 28973 c549650d1442
     1.1 --- a/src/Pure/goal.ML	Thu Oct 16 22:44:27 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Oct 16 22:44:28 2008 +0200
     1.3 @@ -163,15 +163,17 @@
     1.4        |> fold Variable.declare_term (asms @ props)
     1.5        |> Assumption.add_assumes casms
     1.6        ||> Variable.set_body true;
     1.7 +    val sorts = Variable.sorts_of ctxt';
     1.8  
     1.9 -    val stmt = Conjunction.mk_conjunction_balanced cprops;
    1.10 +    val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
    1.11  
    1.12      fun result () =
    1.13        (case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
    1.14          NONE => err "Tactic failed."
    1.15        | SOME st =>
    1.16            let val res = finish st handle THM (msg, _, _) => err msg in
    1.17 -            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
    1.18 +            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
    1.19 +            then Thm.check_shyps sorts res
    1.20              else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
    1.21            end);
    1.22      val res =
    1.23 @@ -250,7 +252,7 @@
    1.24    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.25    THEN' SUBGOAL (fn (t, i) =>
    1.26      if Drule.is_norm_hhf t then all_tac
    1.27 -    else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.28 +    else MetaSimplifier.rewrite_goal_tac Drule.norm_hhf_eqs i);
    1.29  
    1.30  fun compose_hhf_tac th i st =
    1.31    PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;