src/Pure/Isar/calculation.ML
changeset 8649 dc496bb0638f
parent 8634 3f34637cb9c0
child 8807 0046be1769f9
     1.1 --- a/src/Pure/Isar/calculation.ML	Sat Apr 01 20:10:57 2000 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sat Apr 01 20:11:50 2000 +0200
     1.3 @@ -130,11 +130,11 @@
     1.4      fun combine thms =
     1.5        let
     1.6          val ths = thms @ facts;
     1.7 -        val rs = NetRules.inserts (if_none opt_rules []) (get_local_rules state);
     1.8 +        val rs = get_local_rules state;
     1.9          val rules =
    1.10            (case ths of [] => NetRules.rules rs
    1.11            | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
    1.12 -        val ruleq = Seq.of_list rules;
    1.13 +        val ruleq = Seq.of_list (if_none opt_rules [] @ rules);
    1.14        in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
    1.15  
    1.16      val (initial, calculations) =