src/Pure/Isar/calculation.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4    val name = "Isar/calculation";
     1.5    type T = (thm NetRules.T * thm list) * (thm list * int) option;
     1.6  
     1.7 -  fun init thy = (GlobalCalculation.get thy, None);
     1.8 +  fun init thy = (GlobalCalculation.get thy, NONE);
     1.9    fun print ctxt (rs, _) = print_rules ProofContext.pretty_thm ctxt rs;
    1.10  end;
    1.11  
    1.12 @@ -77,15 +77,15 @@
    1.13  
    1.14  fun get_calculation state =
    1.15    (case #2 (LocalCalculation.get (Proof.context_of state)) of
    1.16 -    None => None
    1.17 -  | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    1.18 +    NONE => NONE
    1.19 +  | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    1.20  
    1.21  fun put_calculation thms state =
    1.22    Proof.map_context
    1.23 -    (LocalCalculation.put (get_local_rules state, Some (thms, Proof.level state))) state;
    1.24 +    (LocalCalculation.put (get_local_rules state, SOME (thms, Proof.level state))) state;
    1.25  
    1.26  fun reset_calculation state =
    1.27 -  Proof.map_context (LocalCalculation.put (get_local_rules state, None)) state;
    1.28 +  Proof.map_context (LocalCalculation.put (get_local_rules state, NONE)) state;
    1.29  
    1.30  
    1.31  
    1.32 @@ -101,9 +101,9 @@
    1.33  val trans_add_local = local_att (apfst o NetRules.insert);
    1.34  val trans_del_local = local_att (apfst o NetRules.delete);
    1.35  
    1.36 -val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global None;
    1.37 +val sym_add_global = global_att (apsnd o Drule.add_rule) o ContextRules.elim_query_global NONE;
    1.38  val sym_del_global = global_att (apsnd o Drule.del_rule) o ContextRules.rule_del_global;
    1.39 -val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local None;
    1.40 +val sym_add_local = local_att (apsnd o Drule.add_rule) o ContextRules.elim_query_local NONE;
    1.41  val sym_del_local = local_att (apsnd o Drule.del_rule) o ContextRules.rule_del_local;
    1.42  
    1.43  
    1.44 @@ -164,8 +164,8 @@
    1.45      fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
    1.46  
    1.47      fun combine ths =
    1.48 -      (case opt_rules of Some rules => rules
    1.49 -      | None =>
    1.50 +      (case opt_rules of SOME rules => rules
    1.51 +      | NONE =>
    1.52            (case ths of [] => NetRules.rules (#1 (get_local_rules state))
    1.53            | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
    1.54        |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
    1.55 @@ -174,8 +174,8 @@
    1.56      val facts = Proof.the_facts (assert_sane final state);
    1.57      val (initial, calculations) =
    1.58        (case get_calculation state of
    1.59 -        None => (true, Seq.single facts)
    1.60 -      | Some calc => (false, Seq.map single (combine (calc @ facts))));
    1.61 +        NONE => (true, Seq.single facts)
    1.62 +      | SOME calc => (false, Seq.map single (combine (calc @ facts))));
    1.63    in
    1.64      err_if state (initial andalso final) "No calculation yet";
    1.65      err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.66 @@ -194,8 +194,8 @@
    1.67      val facts = Proof.the_facts (assert_sane final state);
    1.68      val (initial, thms) =
    1.69        (case get_calculation state of
    1.70 -        None => (true, [])
    1.71 -      | Some thms => (false, thms));
    1.72 +        NONE => (true, [])
    1.73 +      | SOME thms => (false, thms));
    1.74      val calc = thms @ facts;
    1.75    in
    1.76      err_if state (initial andalso final) "No calculation yet";