src/Pure/raw_simplifier.ML
changeset 54984 da70ab8531f4
parent 54982 b327bf0dabfb
child 54997 811c35e81ac5
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Jan 10 17:44:41 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Jan 10 21:37:28 2014 +0100
     1.3 @@ -1190,14 +1190,14 @@
     1.4        if mutsimp then mut_impc0 [] ct [] [] ctxt
     1.5        else nonmut_impc ct ctxt
     1.6  
     1.7 -    and rules_of_prem ctxt prem =
     1.8 +    and rules_of_prem prem ctxt =
     1.9        if maxidx_of_term (term_of prem) <> ~1
    1.10        then (trace_cterm ctxt true
    1.11          (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
    1.12 -        prem; ([], NONE))
    1.13 +        prem; (([], NONE), ctxt))
    1.14        else
    1.15 -        let val asm = Thm.assume prem
    1.16 -        in (extract_safe_rrules ctxt asm, SOME asm) end
    1.17 +        let val (asm, ctxt') = Thm.assume_hyps prem ctxt
    1.18 +        in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end
    1.19  
    1.20      and add_rrules (rrss, asms) ctxt =
    1.21        (fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms)
    1.22 @@ -1242,10 +1242,10 @@
    1.23      and mut_impc0 prems concl rrss asms ctxt =
    1.24        let
    1.25          val prems' = strip_imp_prems concl;
    1.26 -        val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems');
    1.27 +        val ((rrss', asms'), ctxt') = fold_map rules_of_prem prems' ctxt |>> split_list;
    1.28        in
    1.29          mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
    1.30 -          (asms @ asms') [] [] [] [] ctxt ~1 ~1
    1.31 +          (asms @ asms') [] [] [] [] ctxt' ~1 ~1
    1.32        end
    1.33  
    1.34      and mut_impc [] concl [] [] prems' rrss' asms' eqns ctxt changed k =
    1.35 @@ -1270,7 +1270,7 @@
    1.36                val tprems = map term_of prems;
    1.37                val i = 1 + fold Integer.max (map (fn p =>
    1.38                  find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
    1.39 -              val (rrs', asm') = rules_of_prem ctxt prem';
    1.40 +              val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt;
    1.41              in
    1.42                mut_impc prems concl rrss asms (prem' :: prems')
    1.43                  (rrs' :: rrss') (asm' :: asms')
    1.44 @@ -1278,7 +1278,7 @@
    1.45                    (take i prems)
    1.46                    (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
    1.47                      (drop i prems, concl))))) :: eqns)
    1.48 -                ctxt (length prems') ~1
    1.49 +                ctxt' (length prems') ~1
    1.50              end)
    1.51  
    1.52      (*legacy code -- only for backwards compatibility*)
    1.53 @@ -1289,7 +1289,9 @@
    1.54          val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
    1.55          val ctxt1 =
    1.56            if not useprem then ctxt
    1.57 -          else add_rrules (apsnd single (apfst single (rules_of_prem ctxt prem1))) ctxt
    1.58 +          else
    1.59 +            let val ((rrs, asm), ctxt') = rules_of_prem prem1 ctxt
    1.60 +            in add_rrules ([rrs], [asm]) ctxt' end;
    1.61        in
    1.62          (case botc skel0 ctxt1 conc of
    1.63            NONE =>