aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
authorblanchet
Fri Feb 14 07:53:46 2014 +0100 (2014-02-14)
changeset 55469b19dd108f0c2
parent 55468 98b25c51e9e5
child 55470 46e6e1d91056
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -82,7 +82,9 @@
     1.4  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
     1.5  done
     1.6  
     1.7 -free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     1.8 +free_constructors case_nat for
     1.9 +    =: "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
    1.10 +  | Suc pred
    1.11    apply atomize_elim
    1.12    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    1.13   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
     2.1 --- a/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     2.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5  subsection {* @{typ bool} is a datatype *}
     2.6  
     2.7 -free_constructors [True, False] case_bool [=]
     2.8 +free_constructors case_bool for =: True | False
     2.9  by auto
    2.10  
    2.11  text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    2.12 @@ -82,7 +82,7 @@
    2.13      else SOME (mk_meta_eq @{thm unit_eq})
    2.14  *}
    2.15  
    2.16 -free_constructors ["()"] case_unit
    2.17 +free_constructors case_unit for "()"
    2.18  by auto
    2.19  
    2.20  text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    2.21 @@ -184,7 +184,7 @@
    2.22  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
    2.23    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    2.24  
    2.25 -free_constructors [Pair] case_prod [] [[fst, snd]]
    2.26 +free_constructors case_prod for Pair fst snd
    2.27  proof -
    2.28    fix P :: bool and p :: "'a \<times> 'b"
    2.29    show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
     3.1 --- a/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     3.2 +++ b/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     3.3 @@ -85,7 +85,9 @@
     3.4    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
     3.5  qed
     3.6  
     3.7 -free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
     3.8 +free_constructors case_sum for
     3.9 +    isl: Inl projl
    3.10 +  | Inr projr
    3.11  by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    3.12  
    3.13  text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     4.3 @@ -92,12 +92,15 @@
     4.4      typ list -> typ list list list -> int list list -> int list list -> int list -> thm list list ->
     4.5      Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
     4.6      local_theory -> gfp_sugar_thms
     4.7 +
     4.8 +  type co_datatype_spec =
     4.9 +    ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    4.10 +    * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
    4.11 +
    4.12    val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    4.13        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    4.14        BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
    4.15 -    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
    4.16 -      * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    4.17 -        mixfix) list) list ->
    4.18 +    (bool * bool) * co_datatype_spec list ->
    4.19      local_theory -> local_theory
    4.20    val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
    4.21        binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
    4.22 @@ -310,18 +313,16 @@
    4.23    reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
    4.24    handle THM _ => thm;
    4.25  
    4.26 -fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs;
    4.27 -fun type_binding_of ((((_, b), _), _), _) = b;
    4.28 -fun map_binding_of (((_, (b, _)), _), _) = b;
    4.29 -fun rel_binding_of (((_, (_, b)), _), _) = b;
    4.30 -fun mixfix_of ((_, mx), _) = mx;
    4.31 -fun ctr_specs_of (_, ctr_specs) = ctr_specs;
    4.32 +type co_datatype_spec =
    4.33 +  ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
    4.34 +  * ((binding, binding * typ, term) ctr_spec * mixfix) list;
    4.35  
    4.36 -fun disc_of ((((disc, _), _), _), _) = disc;
    4.37 -fun ctr_of ((((_, ctr), _), _), _) = ctr;
    4.38 -fun args_of (((_, args), _), _) = args;
    4.39 -fun defaults_of ((_, ds), _) = ds;
    4.40 -fun ctr_mixfix_of (_, mx) = mx;
    4.41 +fun type_args_named_constrained_of_spec ((((ncAs, _), _), _), _) = ncAs;
    4.42 +fun type_binding_of_spec ((((_, b), _), _), _) = b;
    4.43 +fun map_binding_of_spec (((_, (b, _)), _), _) = b;
    4.44 +fun rel_binding_of_spec (((_, (_, b)), _), _) = b;
    4.45 +fun mixfix_of_spec ((_, mx), _) = mx;
    4.46 +fun mixfixed_ctr_specs_of_spec (_, mx_ctr_specs) = mx_ctr_specs;
    4.47  
    4.48  fun add_nesty_bnf_names Us =
    4.49    let
    4.50 @@ -991,22 +992,22 @@
    4.51          ();
    4.52  
    4.53      val nn = length specs;
    4.54 -    val fp_bs = map type_binding_of specs;
    4.55 +    val fp_bs = map type_binding_of_spec specs;
    4.56      val fp_b_names = map Binding.name_of fp_bs;
    4.57      val fp_common_name = mk_common_name fp_b_names;
    4.58 -    val map_bs = map map_binding_of specs;
    4.59 -    val rel_bs = map rel_binding_of specs;
    4.60 +    val map_bs = map map_binding_of_spec specs;
    4.61 +    val rel_bs = map rel_binding_of_spec specs;
    4.62  
    4.63      fun prepare_type_arg (_, (ty, c)) =
    4.64        let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
    4.65          TFree (s, prepare_constraint no_defs_lthy0 c)
    4.66        end;
    4.67  
    4.68 -    val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs;
    4.69 +    val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
    4.70      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    4.71      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    4.72      val num_As = length unsorted_As;
    4.73 -    val set_bss = map (map fst o type_args_named_constrained_of) specs;
    4.74 +    val set_bss = map (map fst o type_args_named_constrained_of_spec) specs;
    4.75  
    4.76      val (((Bs0, Cs), Xs), no_defs_lthy) =
    4.77        no_defs_lthy0
    4.78 @@ -1015,7 +1016,8 @@
    4.79        ||>> mk_TFrees nn
    4.80        ||>> variant_tfrees fp_b_names;
    4.81  
    4.82 -    fun add_fake_type spec = Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec);
    4.83 +    fun add_fake_type spec =
    4.84 +      Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
    4.85  
    4.86      val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
    4.87  
    4.88 @@ -1032,22 +1034,24 @@
    4.89        error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^
    4.90          "datatype specification");
    4.91  
    4.92 -    val mixfixes = map mixfix_of specs;
    4.93 +    val mixfixes = map mixfix_of_spec specs;
    4.94  
    4.95      val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => ()
    4.96        | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
    4.97  
    4.98 -    val ctr_specss = map ctr_specs_of specs;
    4.99 +    val mx_ctr_specss = map mixfixed_ctr_specs_of_spec specs;
   4.100 +    val ctr_specss = map (map fst) mx_ctr_specss;
   4.101 +    val ctr_mixfixess = map (map snd) mx_ctr_specss;
   4.102  
   4.103 -    val disc_bindingss = map (map disc_of) ctr_specss;
   4.104 +    val disc_bindingss = map (map disc_of_ctr_spec) ctr_specss;
   4.105      val ctr_bindingss =
   4.106 -      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
   4.107 -    val ctr_argsss = map (map args_of) ctr_specss;
   4.108 -    val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
   4.109 +      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of_ctr_spec)) fp_b_names
   4.110 +        ctr_specss;
   4.111 +    val ctr_argsss = map (map args_of_ctr_spec) ctr_specss;
   4.112  
   4.113      val sel_bindingsss = map (map (map fst)) ctr_argsss;
   4.114      val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
   4.115 -    val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
   4.116 +    val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss;
   4.117  
   4.118      val (As :: _) :: fake_ctr_Tsss =
   4.119        burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
   4.120 @@ -1249,9 +1253,11 @@
   4.121              val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
   4.122  
   4.123              val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
   4.124 +
   4.125 +            fun ctr_spec_of disc_b ctr0 sel_bs sel_defs = (((disc_b, ctr0), sel_bs), sel_defs);
   4.126 +            val ctr_specs = map4 ctr_spec_of disc_bindings ctrs0 sel_bindingss sel_defaultss;
   4.127            in
   4.128 -            free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
   4.129 -              (sel_bindingss, sel_defaultss))) lthy
   4.130 +            free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy
   4.131            end;
   4.132  
   4.133          fun derive_maps_sets_rels (ctr_sugar as {case_cong, ...} : ctr_sugar, lthy) =
   4.134 @@ -1500,13 +1506,6 @@
   4.135  fun co_datatype_cmd x =
   4.136    define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
   4.137  
   4.138 -val parse_ctr_arg =
   4.139 -  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   4.140 -  (Parse.typ >> pair Binding.empty);
   4.141 -
   4.142 -val parse_defaults =
   4.143 -  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
   4.144 -
   4.145  val parse_type_arg_constrained =
   4.146    Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
   4.147  
   4.148 @@ -1519,15 +1518,18 @@
   4.149    @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   4.150    Scan.succeed [];
   4.151  
   4.152 -val parse_ctr_spec =
   4.153 -  parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg --
   4.154 -  Scan.optional parse_defaults [] -- Parse.opt_mixfix;
   4.155 +val parse_ctr_arg =
   4.156 +  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   4.157 +  (Parse.typ >> pair Binding.empty);
   4.158 +
   4.159 +val parse_ctr_specs =
   4.160 +  Parse.enum1 "|" (parse_ctr_spec parse_binding parse_ctr_arg -- Parse.opt_mixfix);
   4.161  
   4.162  val parse_spec =
   4.163    parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   4.164 -  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
   4.165 +  Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs);
   4.166  
   4.167 -val parse_co_datatype = parse_free_constructors_options -- Parse.and_list1 parse_spec;
   4.168 +val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
   4.169  
   4.170  fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
   4.171  
     5.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Fri Feb 14 07:53:46 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Fri Feb 14 07:53:46 2014 +0100
     5.3 @@ -137,8 +137,6 @@
     5.4  
     5.5    val fold_thms: Proof.context -> thm list -> thm -> thm
     5.6  
     5.7 -  val parse_binding_colon: binding parser
     5.8 -  val parse_opt_binding_colon: binding parser
     5.9    val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
    5.10    val parse_map_rel_bindings: (binding * binding) parser
    5.11  
    5.12 @@ -267,9 +265,6 @@
    5.13      let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
    5.14      in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
    5.15  
    5.16 -val parse_binding_colon = parse_binding --| @{keyword ":"};
    5.17 -val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
    5.18 -
    5.19  val parse_type_arg_constrained =
    5.20    Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
    5.21  
     6.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     6.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     6.3 @@ -53,12 +53,19 @@
     6.4    val dest_case: Proof.context -> string -> typ list -> term ->
     6.5      (ctr_sugar * term list * term list) option
     6.6  
     6.7 +  type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list
     6.8 +
     6.9 +  val disc_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> binding
    6.10 +  val ctr_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'c
    6.11 +  val args_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'a list
    6.12 +  val sel_defaults_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> (binding * 'v) list
    6.13 +
    6.14    val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    6.15 -    (((bool * bool) * term list) * binding) *
    6.16 -      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    6.17 +    ((bool * bool) * binding) * (term, binding, term) ctr_spec list -> local_theory ->
    6.18      ctr_sugar * local_theory
    6.19 -  val parse_free_constructors_options: (bool * bool) parser
    6.20    val parse_bound_term: (binding * string) parser
    6.21 +  val parse_ctr_options: (bool * bool) parser
    6.22 +  val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a, string) ctr_spec parser
    6.23  end;
    6.24  
    6.25  structure Ctr_Sugar : CTR_SUGAR =
    6.26 @@ -278,11 +285,23 @@
    6.27  
    6.28  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    6.29  
    6.30 -fun prepare_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding),
    6.31 -    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    6.32 +type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list;
    6.33 +
    6.34 +fun disc_of_ctr_spec (((disc, _), _), _) = disc;
    6.35 +fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr;
    6.36 +fun args_of_ctr_spec ((_, args), _) = args;
    6.37 +fun sel_defaults_of_ctr_spec (_, ds) = ds;
    6.38 +
    6.39 +fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs)
    6.40 +    no_defs_lthy =
    6.41    let
    6.42      (* TODO: sanity checks on arguments *)
    6.43  
    6.44 +    val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
    6.45 +    val raw_disc_bindings = map disc_of_ctr_spec ctr_specs;
    6.46 +    val raw_sel_bindingss = map args_of_ctr_spec ctr_specs;
    6.47 +    val raw_sel_defaultss = map sel_defaults_of_ctr_spec ctr_specs;
    6.48 +
    6.49      val n = length raw_ctrs;
    6.50      val ks = 1 upto n;
    6.51  
    6.52 @@ -954,29 +973,28 @@
    6.53    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    6.54    prepare_free_constructors Syntax.read_term;
    6.55  
    6.56 -fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    6.57 -
    6.58 -val parse_bindings = parse_bracket_list parse_binding;
    6.59 -val parse_bindingss = parse_bracket_list parse_bindings;
    6.60 +val parse_bound_term = parse_binding --| @{keyword ":"} -- Parse.term;
    6.61  
    6.62 -val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
    6.63 -val parse_bound_terms = parse_bracket_list parse_bound_term;
    6.64 -val parse_bound_termss = parse_bracket_list parse_bound_terms;
    6.65 -
    6.66 -val parse_free_constructors_options =
    6.67 +val parse_ctr_options =
    6.68    Scan.optional (@{keyword "("} |-- Parse.list1
    6.69          (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    6.70        @{keyword ")"}
    6.71        >> (fn js => (member (op =) js 0, member (op =) js 1)))
    6.72      (false, false);
    6.73  
    6.74 +val parse_defaults =
    6.75 +  @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
    6.76 +
    6.77 +fun parse_ctr_spec parse_ctr parse_arg =
    6.78 +  parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg --
    6.79 +  Scan.optional parse_defaults [];
    6.80 +
    6.81 +val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term parse_binding);
    6.82 +
    6.83  val _ =
    6.84    Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    6.85      "register an existing freely generated type's constructors"
    6.86 -    ((parse_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
    6.87 -        @{keyword "]"}) --
    6.88 -      parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    6.89 -        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
    6.90 +    (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
    6.91       >> free_constructors_cmd);
    6.92  
    6.93  end;
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
     7.3 @@ -65,6 +65,8 @@
     7.4    val standard_binding: binding
     7.5    val equal_binding: binding
     7.6    val parse_binding: binding parser
     7.7 +  val parse_binding_colon: binding parser
     7.8 +  val parse_opt_binding_colon: binding parser
     7.9  
    7.10    val ss_only: thm list -> Proof.context -> Proof.context
    7.11  
    7.12 @@ -219,6 +221,8 @@
    7.13  val equal_binding = @{binding "="};
    7.14  
    7.15  val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
    7.16 +val parse_binding_colon = parse_binding --| @{keyword ":"};
    7.17 +val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
    7.18  
    7.19  fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
    7.20