src/Pure/goal.ML
changeset 58950 d07464875dd4
parent 58837 e84d900cd287
child 58963 26bf09b95dda
     1.1 --- a/src/Pure/goal.ML	Sat Nov 08 17:39:01 2014 +0100
     1.2 +++ b/src/Pure/goal.ML	Sat Nov 08 21:31:51 2014 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4  (* normal form *)
     1.5  
     1.6  fun norm_result ctxt =
     1.7 -  Drule.flexflex_unique
     1.8 +  Drule.flexflex_unique (SOME ctxt)
     1.9    #> Raw_Simplifier.norm_hhf_protect ctxt
    1.10    #> Thm.strip_shyps
    1.11    #> Drule.zero_var_indexes;
    1.12 @@ -144,7 +144,7 @@
    1.13        cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
    1.14        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
    1.15      val global_result = result |> Future.map
    1.16 -      (Drule.flexflex_unique #>
    1.17 +      (Drule.flexflex_unique (SOME ctxt) #>
    1.18          Thm.adjust_maxidx_thm ~1 #>
    1.19          Drule.implies_intr_list assms #>
    1.20          Drule.forall_intr_list fixes #>
    1.21 @@ -216,12 +216,13 @@
    1.22                Theory.subthy (theory_of_thm st, thy) orelse err "Bad background theory of goal state";
    1.23              val res =
    1.24                (finish ctxt' st
    1.25 -                |> Drule.flexflex_unique
    1.26 +                |> Drule.flexflex_unique (SOME ctxt')
    1.27                  |> Thm.check_shyps sorts
    1.28                  |> Thm.check_hyps (Context.Proof ctxt'))
    1.29                handle THM (msg, _, _) => err msg | ERROR msg => err msg;
    1.30            in
    1.31 -            if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res] then res
    1.32 +            if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res]
    1.33 +            then res
    1.34              else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
    1.35            end);
    1.36      val res =