outer syntax: no simps;
authorwenzelm
Thu Apr 13 17:49:42 2000 +0200 (2000-04-13)
changeset 871100ec2ba9174d
parent 8710 d90bab9d001b
child 8712 cbc02c7d8229
outer syntax: no simps;
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Apr 13 17:49:08 2000 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Apr 13 17:49:42 2000 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  
     1.5  fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
     1.6  
     1.7 -fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
     1.8 +fun gen_add_recdef tfl_fn prep_att app_thms raw_name R eq_srcs opt_ss raw_congs thy =
     1.9    let
    1.10      val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.11      val bname = Sign.base_name name;
    1.12 @@ -83,7 +83,7 @@
    1.13  
    1.14      val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
    1.15      val eq_atts = map (map (prep_att thy)) raw_eq_atts;
    1.16 -    val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    1.17 +    val ss = if_none opt_ss (Simplifier.simpset_of thy);
    1.18      val (thy, congs) = thy |> app_thms raw_congs;
    1.19  
    1.20      val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    1.21 @@ -103,10 +103,9 @@
    1.22        |> Theory.parent_path;
    1.23    in (thy, result) end;
    1.24  
    1.25 -val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
    1.26 -val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
    1.27 -  (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
    1.28 -val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
    1.29 +val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
    1.30 +val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute IsarThy.apply_theorems;
    1.31 +val add_recdef_i = gen_add_recdef Tfl.define_i (K I) IsarThy.apply_theorems_i;
    1.32  
    1.33  
    1.34  
    1.35 @@ -147,9 +146,8 @@
    1.36  
    1.37  val recdef_decl =
    1.38    P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) --
    1.39 -  Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
    1.40 -  Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
    1.41 -  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map P.triple_swap eqs) ss congs);
    1.42 +  Scan.optional (P.$$$ "congs" |-- P.!!! P.xthms1) []
    1.43 +  >> (fn (((f, R), eqs), congs) => #1 o add_recdef_x f R (map P.triple_swap eqs) None congs);
    1.44  
    1.45  val recdefP =
    1.46    OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl