(RAW_)METHOD_CASES: RuleCases.tactic;
authorwenzelm
Fri Jun 17 18:33:33 2005 +0200 (2005-06-17)
changeset 164486c45c5416b79
parent 16447 01c4b30f91e9
child 16449 d0dc9a301e37
(RAW_)METHOD_CASES: RuleCases.tactic;
accomodate change of TheoryDataFun;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Fri Jun 17 18:33:32 2005 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Jun 17 18:33:33 2005 +0200
     1.3 @@ -18,11 +18,9 @@
     1.4    type src
     1.5    val trace: Proof.context -> thm list -> unit
     1.6    val RAW_METHOD: (thm list -> tactic) -> Proof.method
     1.7 -  val RAW_METHOD_CASES:
     1.8 -    (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> Proof.method
     1.9 +  val RAW_METHOD_CASES: (thm list -> RuleCases.tactic) -> Proof.method
    1.10    val METHOD: (thm list -> tactic) -> Proof.method
    1.11 -  val METHOD_CASES:
    1.12 -    (thm list -> thm -> (thm * (string * RuleCases.T option) list) Seq.seq) -> Proof.method
    1.13 +  val METHOD_CASES: (thm list -> RuleCases.tactic) -> Proof.method
    1.14    val SIMPLE_METHOD: tactic -> Proof.method
    1.15    val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> Proof.method
    1.16    val fail: Proof.method
    1.17 @@ -502,15 +500,15 @@
    1.18  
    1.19  (* data kind 'Isar/methods' *)
    1.20  
    1.21 -structure MethodsDataArgs =
    1.22 -struct
    1.23 +structure MethodsData = TheoryDataFun
    1.24 +(struct
    1.25    val name = "Isar/methods";
    1.26    type T = (((src -> Proof.context -> Proof.method) * string) * stamp) NameSpace.table;
    1.27  
    1.28    val empty = NameSpace.empty_table;
    1.29    val copy = I;
    1.30 -  val prep_ext = I;
    1.31 -  fun merge tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    1.32 +  val extend = I;
    1.33 +  fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
    1.34      error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
    1.35  
    1.36    fun print _ meths =
    1.37 @@ -521,9 +519,8 @@
    1.38        [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    1.39        |> Pretty.chunks |> Pretty.writeln
    1.40      end;
    1.41 -end;
    1.42 +end);
    1.43  
    1.44 -structure MethodsData = TheoryDataFun(MethodsDataArgs);
    1.45  val _ = Context.add_setup [MethodsData.init];
    1.46  val print_methods = MethodsData.print;
    1.47