src/Pure/Isar/context_rules.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/Isar/context_rules.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4    Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
     1.5  
     1.6  fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
     1.7 -  let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
     1.8 +  let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
     1.9      make_rules (next - 1) ((w, ((i, b), th)) :: rules)
    1.10        (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
    1.11    end;
    1.12 @@ -113,7 +113,7 @@
    1.13    let
    1.14      fun prt_kind (i, b) =
    1.15        Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
    1.16 -        (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
    1.17 +        (mapfilter (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
    1.18            (sort (Int.compare o pairself fst) rules));
    1.19    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    1.20  
    1.21 @@ -254,14 +254,14 @@
    1.22  fun modifier att (x, ths) =
    1.23    #1 (Thm.applys_attributes ((x, rev ths), [att]));
    1.24  
    1.25 -val addXIs_global = modifier (intro_query_global None);
    1.26 -val addXEs_global = modifier (elim_query_global None);
    1.27 -val addXDs_global = modifier (dest_query_global None);
    1.28 +val addXIs_global = modifier (intro_query_global NONE);
    1.29 +val addXEs_global = modifier (elim_query_global NONE);
    1.30 +val addXDs_global = modifier (dest_query_global NONE);
    1.31  val delrules_global = modifier rule_del_global;
    1.32  
    1.33 -val addXIs_local = modifier (intro_query_local None);
    1.34 -val addXEs_local = modifier (elim_query_local None);
    1.35 -val addXDs_local = modifier (dest_query_local None);
    1.36 +val addXIs_local = modifier (intro_query_local NONE);
    1.37 +val addXEs_local = modifier (elim_query_local NONE);
    1.38 +val addXDs_local = modifier (dest_query_local NONE);
    1.39  val delrules_local = modifier rule_del_local;
    1.40  
    1.41