tuned signature;
authorwenzelm
Wed Jun 22 10:40:53 2016 +0200 (2016-06-22)
changeset 63344c9910404cc8a
parent 63343 fb5d8a50c641
child 63345 70b2313f9c52
tuned signature;
tuned;
src/HOL/Library/simps_case_conv.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/proof.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 10:09:20 2016 +0200
     1.2 +++ b/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 10:40:53 2016 +0200
     1.3 @@ -136,8 +136,8 @@
     1.4        let
     1.5          val frees = fold Term.add_frees pat []
     1.6          val abs_rhs = fold absfree frees rhs
     1.7 -        val ((f,def), lthy') = Local_Defs.add_def
     1.8 -          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
     1.9 +        val ([(f, (_, def))], lthy') = lthy
    1.10 +          |> Local_Defs.define [((Binding.name name, Mixfix.NoSyn), (Thm.empty_binding, abs_rhs))]
    1.11        in ((list_comb (f, map Free (rev frees)), def), lthy') end
    1.12  
    1.13      val ((def_ts, def_thms), ctxt2) =
     2.1 --- a/src/Pure/Isar/generic_target.ML	Wed Jun 22 10:09:20 2016 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Jun 22 10:40:53 2016 +0200
     2.3 @@ -241,8 +241,8 @@
     2.4        |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
     2.5  
     2.6      (*local definition*)
     2.7 -    val ((lhs, local_def), lthy3) = lthy2
     2.8 -      |> Local_Defs.add_def ((b, NoSyn), lhs');
     2.9 +    val ([(lhs, (_, local_def))], lthy3) = lthy2
    2.10 +      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))];
    2.11  
    2.12      (*result*)
    2.13      val def =
     3.1 --- a/src/Pure/Isar/local_defs.ML	Wed Jun 22 10:09:20 2016 +0200
     3.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Jun 22 10:40:53 2016 +0200
     3.3 @@ -10,9 +10,8 @@
     3.4    val abs_def: term -> (string * typ) * term
     3.5    val expand: cterm list -> thm -> thm
     3.6    val def_export: Assumption.export
     3.7 -  val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
     3.8 +  val define: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
     3.9      (term * (string * thm)) list * Proof.context
    3.10 -  val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
    3.11    val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
    3.12      (term * term) * Proof.context
    3.13    val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
    3.14 @@ -66,7 +65,9 @@
    3.15    let
    3.16      val (bs, rhss) = split_list args;
    3.17      val Ts = map Term.fastype_of rhss;
    3.18 -    val (xs, _) = Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts) ctxt;
    3.19 +    val (xs, _) = ctxt
    3.20 +      |> Context_Position.set_visible false
    3.21 +      |> Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts);
    3.22      val lhss = ListPair.map Free (xs, Ts);
    3.23    in map Logic.mk_equals (lhss ~~ rhss) end;
    3.24  
    3.25 @@ -94,13 +95,13 @@
    3.26  fun def_export _ defs = (expand defs, expand_term defs);
    3.27  
    3.28  
    3.29 -(* add defs *)
    3.30 +(* define *)
    3.31  
    3.32 -fun add_defs defs ctxt =
    3.33 +fun define defs ctxt =
    3.34    let
    3.35      val ((xs, mxs), specs) = defs |> split_list |>> split_list;
    3.36      val (bs, rhss) = specs |> split_list;
    3.37 -    val eqs = mk_def (Context_Position.set_visible false ctxt) (xs ~~ rhss);
    3.38 +    val eqs = mk_def ctxt (xs ~~ rhss);
    3.39      val lhss = map (fst o Logic.dest_equals) eqs;
    3.40    in
    3.41      ctxt
    3.42 @@ -110,10 +111,6 @@
    3.43      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
    3.44    end;
    3.45  
    3.46 -fun add_def (var, rhs) ctxt =
    3.47 -  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
    3.48 -  in ((lhs, th), ctxt') end;
    3.49 -
    3.50  
    3.51  (* fixed_abbrev *)
    3.52  
     4.1 --- a/src/Pure/Isar/proof.ML	Wed Jun 22 10:09:20 2016 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Wed Jun 22 10:40:53 2016 +0200
     4.3 @@ -699,7 +699,7 @@
     4.4          let
     4.5            val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
     4.6              ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
     4.7 -        in map_context_result (Local_Defs.add_defs defs) end))
     4.8 +        in map_context_result (Local_Defs.define defs) end))
     4.9      |-> (set_facts o map (#2 o #2))
    4.10    end;
    4.11  
    4.12 @@ -868,7 +868,7 @@
    4.13      val derived_def = Local_Defs.derived_def ctxt {conditional = false};
    4.14      val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
    4.15      val defs2 = match_defs decls defs1;
    4.16 -    val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
    4.17 +    val (defs3, defs_ctxt) = Local_Defs.define defs2 ctxt;
    4.18  
    4.19      (*notes*)
    4.20      val def_thmss =
     5.1 --- a/src/Tools/induct.ML	Wed Jun 22 10:09:20 2016 +0200
     5.2 +++ b/src/Tools/induct.ML	Wed Jun 22 10:40:53 2016 +0200
     5.3 @@ -725,7 +725,7 @@
     5.4      fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
     5.5        | add (SOME (SOME x, (t, _))) ctxt =
     5.6            let val ([(lhs, (_, th))], ctxt') =
     5.7 -            Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
     5.8 +            Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
     5.9            in ((SOME lhs, [th]), ctxt') end
    5.10        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
    5.11        | add (SOME (NONE, (t, _))) ctxt =
    5.12 @@ -733,7 +733,7 @@
    5.13              val (s, _) = Name.variant "x" (Variable.names_of ctxt);
    5.14              val x = Binding.name s;
    5.15              val ([(lhs, (_, th))], ctxt') = ctxt
    5.16 -              |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
    5.17 +              |> Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))];
    5.18            in ((SOME lhs, [th]), ctxt') end
    5.19        | add NONE ctxt = ((NONE, []), ctxt);
    5.20    in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;