--- a/src/Pure/Isar/context_rules.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/Isar/context_rules.ML Sun Feb 13 17:15:14 2005 +0100
@@ -95,7 +95,7 @@
Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
- let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in
+ let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
make_rules (next - 1) ((w, ((i, b), th)) :: rules)
(map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
end;
@@ -113,7 +113,7 @@
let
fun prt_kind (i, b) =
Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
- (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None)
+ (mapfilter (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
(sort (Int.compare o pairself fst) rules));
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
@@ -254,14 +254,14 @@
fun modifier att (x, ths) =
#1 (Thm.applys_attributes ((x, rev ths), [att]));
-val addXIs_global = modifier (intro_query_global None);
-val addXEs_global = modifier (elim_query_global None);
-val addXDs_global = modifier (dest_query_global None);
+val addXIs_global = modifier (intro_query_global NONE);
+val addXEs_global = modifier (elim_query_global NONE);
+val addXDs_global = modifier (dest_query_global NONE);
val delrules_global = modifier rule_del_global;
-val addXIs_local = modifier (intro_query_local None);
-val addXEs_local = modifier (elim_query_local None);
-val addXDs_local = modifier (dest_query_local None);
+val addXIs_local = modifier (intro_query_local NONE);
+val addXEs_local = modifier (elim_query_local NONE);
+val addXDs_local = modifier (dest_query_local NONE);
val delrules_local = modifier rule_del_local;