tuned NetRules;
authorwenzelm
Mon Oct 15 20:36:48 2001 +0200 (2001-10-15)
changeset 11784b66b198ee29a
parent 11783 aee100a086b1
child 11785 3087d6f19adc
tuned NetRules;
src/Pure/Isar/calculation.ML
src/Pure/Isar/induct_attrib.ML
     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  
     2.1 --- a/src/Pure/Isar/induct_attrib.ML	Mon Oct 15 20:36:04 2001 +0200
     2.2 +++ b/src/Pure/Isar/induct_attrib.ML	Mon Oct 15 20:36:48 2001 +0200
     2.3 @@ -84,7 +84,7 @@
     2.4  type rules = (string * thm) NetRules.T;
     2.5  
     2.6  val init_rules = NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2
     2.7 -  andalso Thm.eq_thm (th1, th2));
     2.8 +  andalso Thm.eq_thm (th1, th2)) (K 0);
     2.9  
    2.10  fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
    2.11  
    2.12 @@ -153,7 +153,7 @@
    2.13  
    2.14  
    2.15  fun find_rules which how ctxt x =
    2.16 -  map snd (NetRules.may_unify (which (LocalInduct.get ctxt)) (how x));
    2.17 +  map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
    2.18  
    2.19  val find_casesT = find_rules (#1 o #1) encode_type;
    2.20  val find_casesS = find_rules (#2 o #1) Thm.concl_of;