src/Pure/Isar/calculation.ML
changeset 11784 b66b198ee29a
parent 11097 c1be9f2dff4c
child 12021 8809efda06d3
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Oct 15 20:36:04 2001 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Oct 15 20:36:48 2001 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    val name = "Isar/calculation";
     1.5    type T = thm NetRules.T
     1.6  
     1.7 -  val empty = NetRules.init_elim;
     1.8 +  val empty = NetRules.elim;
     1.9    val copy = I;
    1.10    val prep_ext = I;
    1.11    val merge = NetRules.merge;
    1.12 @@ -131,7 +131,7 @@
    1.13        (case opt_rules of Some rules => rules
    1.14        | None =>
    1.15            (case ths of [] => NetRules.rules (get_local_rules state)
    1.16 -          | th :: _ => NetRules.may_unify (get_local_rules state) (strip_assums_concl th)))
    1.17 +          | th :: _ => NetRules.retrieve (get_local_rules state) (strip_assums_concl th)))
    1.18        |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
    1.19        |> Seq.filter (not o projection ths);
    1.20