src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55468 98b25c51e9e5
parent 55464 56fa33537869
child 55469 b19dd108f0c2
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -53,11 +53,11 @@
     1.4    val dest_case: Proof.context -> string -> typ list -> term ->
     1.5      (ctr_sugar * term list * term list) option
     1.6  
     1.7 -  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     1.8 +  val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     1.9      (((bool * bool) * term list) * binding) *
    1.10        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    1.11      ctr_sugar * local_theory
    1.12 -  val parse_wrap_free_constructors_options: (bool * bool) parser
    1.13 +  val parse_free_constructors_options: (bool * bool) parser
    1.14    val parse_bound_term: (binding * string) parser
    1.15  end;
    1.16  
    1.17 @@ -278,8 +278,8 @@
    1.18  
    1.19  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    1.20  
    1.21 -fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs),
    1.22 -    raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    1.23 +fun prepare_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding),
    1.24 +    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    1.25    let
    1.26      (* TODO: sanity checks on arguments *)
    1.27  
    1.28 @@ -946,13 +946,13 @@
    1.29      (goalss, after_qed, lthy')
    1.30    end;
    1.31  
    1.32 -fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
    1.33 +fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
    1.34    map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
    1.35 -  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
    1.36 +  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I);
    1.37  
    1.38 -val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
    1.39 +val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
    1.40    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    1.41 -  prepare_wrap_free_constructors Syntax.read_term;
    1.42 +  prepare_free_constructors Syntax.read_term;
    1.43  
    1.44  fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    1.45  
    1.46 @@ -963,7 +963,7 @@
    1.47  val parse_bound_terms = parse_bracket_list parse_bound_term;
    1.48  val parse_bound_termss = parse_bracket_list parse_bound_terms;
    1.49  
    1.50 -val parse_wrap_free_constructors_options =
    1.51 +val parse_free_constructors_options =
    1.52    Scan.optional (@{keyword "("} |-- Parse.list1
    1.53          (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    1.54        @{keyword ")"}
    1.55 @@ -971,12 +971,12 @@
    1.56      (false, false);
    1.57  
    1.58  val _ =
    1.59 -  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
    1.60 -    "wrap an existing freely generated type's constructors"
    1.61 -    ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
    1.62 +  Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    1.63 +    "register an existing freely generated type's constructors"
    1.64 +    ((parse_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
    1.65          @{keyword "]"}) --
    1.66        parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    1.67          Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
    1.68 -     >> wrap_free_constructors_cmd);
    1.69 +     >> free_constructors_cmd);
    1.70  
    1.71  end;