src/Pure/Isar/context_rules.ML
changeset 16424 18a07ad8fea8
parent 15973 5fd94d84470f
child 16512 1fa048f2a590
     1.1 --- a/src/Pure/Isar/context_rules.ML	Fri Jun 17 18:33:03 2005 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Jun 17 18:33:05 2005 +0200
     1.3 @@ -126,9 +126,9 @@
     1.4  
     1.5    val empty = make_rules ~1 [] empty_netpairs ([], []);
     1.6    val copy = I;
     1.7 -  val prep_ext = I;
     1.8 +  val extend = I;
     1.9  
    1.10 -  fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
    1.11 +  fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
    1.12        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
    1.13      let
    1.14        val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
    1.15 @@ -147,15 +147,14 @@
    1.16  val _ = Context.add_setup [GlobalRules.init];
    1.17  val print_global_rules = GlobalRules.print;
    1.18  
    1.19 -structure LocalRulesArgs =
    1.20 -struct
    1.21 +structure LocalRules = ProofDataFun
    1.22 +(struct
    1.23    val name = GlobalRulesArgs.name;
    1.24    type T = GlobalRulesArgs.T;
    1.25    val init = GlobalRules.get;
    1.26    val print = print_rules ProofContext.pretty_thm;
    1.27 -end;
    1.28 +end);
    1.29  
    1.30 -structure LocalRules = ProofDataFun(LocalRulesArgs);
    1.31  val _ = Context.add_setup [LocalRules.init];
    1.32  val print_local_rules = LocalRules.print;
    1.33  
    1.34 @@ -175,22 +174,25 @@
    1.35        if k = k' then untaglist rest
    1.36        else x :: untaglist rest;
    1.37  
    1.38 -fun orderlist brls = 
    1.39 -    untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    1.40 -fun orderlist_no_weight brls = 
    1.41 -    untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    1.42 +fun orderlist brls =
    1.43 +  untaglist (sort (prod_ord Int.compare Int.compare o pairself fst) brls);
    1.44 +
    1.45 +fun orderlist_no_weight brls =
    1.46 +  untaglist (sort (Int.compare o pairself (snd o fst)) brls);
    1.47  
    1.48  fun may_unify weighted t net =
    1.49    map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
    1.50  
    1.51  fun find_erules _ [] = K []
    1.52    | find_erules w (fact :: _) = may_unify w (Logic.strip_assums_concl (Thm.prop_of fact));
    1.53 +
    1.54  fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal);
    1.55  
    1.56  fun find_rules_netpair weighted facts goal (inet, enet) =
    1.57    find_erules weighted facts enet @ find_irules weighted goal inet;
    1.58  
    1.59 -fun find_rules weighted facts goals = map (find_rules_netpair weighted facts goals) o netpairs;
    1.60 +fun find_rules weighted facts goals =
    1.61 +  map (find_rules_netpair weighted facts goals) o netpairs;
    1.62  
    1.63  
    1.64  (* wrappers *)
    1.65 @@ -268,5 +270,4 @@
    1.66  val addXDs_local = modifier (dest_query_local NONE);
    1.67  val delrules_local = modifier rule_del_local;
    1.68  
    1.69 -
    1.70  end;