tuned interfaces;
authorwenzelm
Fri Oct 19 20:57:14 2007 +0200 (2007-10-19 ago)
changeset 2510426b9a7db3386
parent 25103 1ee419a5a30f
child 25105 c9f67836c4d8
tuned interfaces;
src/Pure/Isar/class.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 19 19:45:31 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 19 20:57:14 2007 +0200
     1.3 @@ -20,9 +20,9 @@
     1.4    val these_params: theory -> sort -> (string * (string * typ)) list
     1.5    val init: class -> Proof.context -> Proof.context
     1.6    val add_logical_const: string -> Markup.property list
     1.7 -    -> (string * mixfix) * term -> theory -> string * theory
     1.8 +    -> (string * mixfix) * term -> theory -> theory
     1.9    val add_syntactic_const: string -> Syntax.mode -> Markup.property list
    1.10 -    -> (string * mixfix) * term -> theory -> string * theory
    1.11 +    -> (string * mixfix) * term -> theory -> theory
    1.12    val refresh_syntax: class -> Proof.context -> Proof.context
    1.13    val intro_classes_tac: thm list -> tactic
    1.14    val default_intro_classes_tac: thm list -> tactic
    1.15 @@ -827,7 +827,6 @@
    1.16            #> register_operation class ((c', (dict, dict')), SOME (Thm.varifyT def)))
    1.17      |> Sign.restore_naming thy
    1.18      |> Sign.add_const_constraint (c', SOME ty')
    1.19 -    |> pair c'
    1.20    end;
    1.21  
    1.22  
    1.23 @@ -872,7 +871,6 @@
    1.24      |> Sign.notation true prmode [(Const (c', ty'), mx)]
    1.25      |> register_operation class ((c', (dict', dict'')), NONE)
    1.26      |> Sign.restore_naming thy
    1.27 -    |> pair c'
    1.28    end;
    1.29  
    1.30  end;
     2.1 --- a/src/Pure/Isar/local_defs.ML	Fri Oct 19 19:45:31 2007 +0200
     2.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Oct 19 20:57:14 2007 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4    val def_export: Assumption.export
     2.5    val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     2.6      (term * (bstring * thm)) list * Proof.context
     2.7 -  val add_def: (string * mixfix) * term -> Proof.context -> (term * (bstring * thm)) * Proof.context
     2.8 +  val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
     2.9    val export: Proof.context -> Proof.context -> thm -> thm list * thm
    2.10    val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
    2.11    val trans_terms: Proof.context -> thm list -> thm
    2.12 @@ -101,7 +101,9 @@
    2.13      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
    2.14    end;
    2.15  
    2.16 -fun add_def (var, rhs) = add_defs [(var, (("", []), rhs))] #>> the_single;
    2.17 +fun add_def (var, rhs) ctxt =
    2.18 +  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (("", []), rhs))] ctxt
    2.19 +  in ((lhs, th), ctxt') end;
    2.20  
    2.21  
    2.22  (* specific export -- result based on educated guessing *)
     3.1 --- a/src/Pure/Isar/local_theory.ML	Fri Oct 19 19:45:31 2007 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Oct 19 20:57:14 2007 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     3.5      -> (term list * (bstring * thm list) list) * local_theory
     3.6    val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
     3.7 -    (term * (bstring * thm)) * local_theory
     3.8 +    (term * thm) * local_theory
     3.9    val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    3.10      (term * (bstring * thm)) * local_theory
    3.11    val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    3.12 @@ -57,8 +57,7 @@
    3.13    axioms: string ->
    3.14      ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
    3.15      -> (term list * (bstring * thm list) list) * local_theory,
    3.16 -  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
    3.17 -    (term * (bstring * thm)) * local_theory,
    3.18 +  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * thm) * local_theory,
    3.19    define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
    3.20      (term * (bstring * thm)) * local_theory,
    3.21    notes: string ->