1.1 --- a/src/HOL/Tools/Function/function.ML	Sat Aug 13 21:28:01 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Aug 13 22:04:07 2011 +0200
     1.3 @@ -125,9 +125,7 @@
     1.4            pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
     1.5            fs=fs, R=R, defname=defname, is_partial=true }
     1.6  
     1.7 -        val _ =
     1.8 -          if not is_external then ()
     1.9 -          else Specification.print_consts lthy (K false) (map fst fixes)
    1.10 +        val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
    1.11        in
    1.12          (info, 
    1.13           lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 21:28:01 2011 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 22:04:07 2011 +0200
     2.3 @@ -218,11 +218,11 @@
     2.4  (* constant definitions and abbreviations *)
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.local_theory "definition" "constant definition" Keyword.thy_decl
     2.8 -    (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args));
     2.9 +  Outer_Syntax.local_theory' "definition" "constant definition" Keyword.thy_decl
    2.10 +    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
    2.11  
    2.12  val _ =
    2.13 -  Outer_Syntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
    2.14 +  Outer_Syntax.local_theory' "abbreviation" "constant abbreviation" Keyword.thy_decl
    2.15      (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
    2.16        >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
    2.17  
    2.18 @@ -263,18 +263,18 @@
    2.19  (* theorems *)
    2.20  
    2.21  fun theorems kind =
    2.22 -  Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
    2.23 +  Parse_Spec.name_facts >> (fn args => #2 oo Specification.theorems_cmd kind args);
    2.24  
    2.25  val _ =
    2.26 -  Outer_Syntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
    2.27 +  Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
    2.28  
    2.29  val _ =
    2.30 -  Outer_Syntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
    2.31 +  Outer_Syntax.local_theory' "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
    2.32  
    2.33  val _ =
    2.34 -  Outer_Syntax.local_theory "declare" "declare theorems" Keyword.thy_decl
    2.35 +  Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl
    2.36      (Parse.and_list1 Parse_Spec.xthms1
    2.37 -      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
    2.38 +      >> (fn args => #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
    2.39  
    2.40  
    2.41  (* name space entry path *)

     3.1 --- a/src/Pure/Isar/proof_display.ML	Sat Aug 13 21:28:01 2011 +0200
     3.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Aug 13 22:04:07 2011 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4    val print_theory: theory -> unit
     3.5    val string_of_rule: Proof.context -> string -> thm -> string
     3.6    val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
     3.7 -  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
     3.8 +  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
     3.9  end
    3.10  
    3.11  structure Proof_Display: PROOF_DISPLAY =
    3.12 @@ -115,13 +115,17 @@
    3.13  
    3.14  fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
    3.15  
    3.16 -in
    3.17 -
    3.18  fun pretty_consts ctxt pred cs =
    3.19    (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
    3.20      [] => pretty_vars ctxt "constants" cs
    3.21    | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
    3.22  
    3.23 +in
    3.24 +
    3.25 +fun print_consts do_print ctxt pred cs =
    3.26 +  if not do_print orelse null cs then ()
    3.27 +  else Pretty.writeln (pretty_consts ctxt pred cs);
    3.28 +
    3.29  end;
    3.30  
    3.31  end;

     4.1 --- a/src/Pure/Isar/specification.ML	Sat Aug 13 21:28:01 2011 +0200
     4.2 +++ b/src/Pure/Isar/specification.ML	Sat Aug 13 22:04:07 2011 +0200
     4.3 @@ -7,7 +7,6 @@
     4.4  
     4.5  signature SPECIFICATION =
     4.6  sig
     4.7 -  val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
     4.8    val check_spec:
     4.9      (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
    4.10      (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
    4.11 @@ -37,23 +36,26 @@
    4.12    val definition:
    4.13      (binding * typ option * mixfix) option * (Attrib.binding * term) ->
    4.14      local_theory -> (term * (string * thm)) * local_theory
    4.15 +  val definition':
    4.16 +    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
    4.17 +    bool -> local_theory -> (term * (string * thm)) * local_theory
    4.18    val definition_cmd:
    4.19      (binding * string option * mixfix) option * (Attrib.binding * string) ->
    4.20 -    local_theory -> (term * (string * thm)) * local_theory
    4.21 +    bool -> local_theory -> (term * (string * thm)) * local_theory
    4.22    val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
    4.23 -    local_theory -> local_theory
    4.24 +    bool -> local_theory -> local_theory
    4.25    val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
    4.26 -    local_theory -> local_theory
    4.27 +    bool -> local_theory -> local_theory
    4.28    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    4.29    val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    4.30    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    4.31    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    4.32    val theorems: string ->
    4.33      (Attrib.binding * (thm list * Attrib.src list) list) list ->
    4.34 -    local_theory -> (string * thm list) list * local_theory
    4.35 +    bool -> local_theory -> (string * thm list) list * local_theory
    4.36    val theorems_cmd: string ->
    4.37      (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
    4.38 -    local_theory -> (string * thm list) list * local_theory
    4.39 +    bool -> local_theory -> (string * thm list) list * local_theory
    4.40    val theorem: string -> Method.text option ->
    4.41      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    4.42      Element.context_i list -> Element.statement_i ->
    4.43 @@ -76,12 +78,6 @@
    4.44  structure Specification: SPECIFICATION =
    4.45  struct
    4.46  
    4.47 -(* diagnostics *)
    4.48 -
    4.49 -fun print_consts _ _ [] = ()
    4.50 -  | print_consts ctxt pred cs = Pretty.writeln (Proof_Display.pretty_consts ctxt pred cs);
    4.51 -
    4.52 -
    4.53  (* prepare specification *)
    4.54  
    4.55  local
    4.56 @@ -166,7 +162,7 @@
    4.57  
    4.58  (* axiomatization -- within global theory *)
    4.59  
    4.60 -fun gen_axioms do_print prep raw_vars raw_specs thy =
    4.61 +fun gen_axioms prep raw_vars raw_specs thy =
    4.62    let
    4.63      val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
    4.64      val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
    4.65 @@ -188,13 +184,10 @@
    4.66        |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
    4.67        |> Local_Theory.notes axioms;
    4.68  
    4.69 -    val _ =
    4.70 -      if not do_print then ()
    4.71 -      else print_consts facts_lthy (K false) xs;
    4.72    in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
    4.73  
    4.74 -val axiomatization = gen_axioms false check_specification;
    4.75 -val axiomatization_cmd = gen_axioms true read_specification;
    4.76 +val axiomatization = gen_axioms check_specification;
    4.77 +val axiomatization_cmd = gen_axioms read_specification;
    4.78  
    4.79  fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd);
    4.80  fun axiom_cmd (b, ax) = axiomatization_cmd [] [(b, [ax])] #>> (hd o hd o snd);
    4.81 @@ -202,7 +195,7 @@
    4.82  
    4.83  (* definition *)
    4.84  
    4.85 -fun gen_def do_print prep (raw_var, raw_spec) lthy =
    4.86 +fun gen_def prep (raw_var, raw_spec) int lthy =
    4.87    let
    4.88      val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
    4.89      val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
    4.90 @@ -228,18 +221,18 @@
    4.91          [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
    4.92  
    4.93      val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
    4.94 -    val _ =
    4.95 -      if not do_print then ()
    4.96 -      else print_consts lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    4.97 +
    4.98 +    val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    4.99    in ((lhs, (def_name, th')), lthy4) end;
   4.100  
   4.101 -val definition = gen_def false check_free_spec;
   4.102 -val definition_cmd = gen_def true read_free_spec;
   4.103 +val definition' = gen_def check_free_spec;
   4.104 +fun definition spec = definition' spec false;
   4.105 +val definition_cmd = gen_def read_free_spec;
   4.106  
   4.107  
   4.108  (* abbreviation *)
   4.109  
   4.110 -fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
   4.111 +fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
   4.112    let
   4.113      val ((vars, [(_, prop)]), _) =
   4.114        prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
   4.115 @@ -260,11 +253,11 @@
   4.116        |> Local_Theory.abbrev mode (var, rhs) |> snd
   4.117        |> Proof_Context.restore_syntax_mode lthy;
   4.118  
   4.119 -    val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
   4.120 +    val _ = Proof_Display.print_consts int lthy' (K false) [(x, T)];
   4.121    in lthy' end;
   4.122  
   4.123 -val abbreviation = gen_abbrev false check_free_spec;
   4.124 -val abbreviation_cmd = gen_abbrev true read_free_spec;
   4.125 +val abbreviation = gen_abbrev check_free_spec;
   4.126 +val abbreviation_cmd = gen_abbrev read_free_spec;
   4.127  
   4.128  
   4.129  (* notation *)
   4.130 @@ -290,14 +283,14 @@
   4.131  
   4.132  (* fact statements *)
   4.133  
   4.134 -fun gen_theorems prep_fact prep_att kind raw_facts lthy =
   4.135 +fun gen_theorems prep_fact prep_att kind raw_facts int lthy =
   4.136    let
   4.137      val attrib = prep_att (Proof_Context.theory_of lthy);
   4.138      val facts = raw_facts |> map (fn ((name, atts), bs) =>
   4.139        ((name, map attrib atts),
   4.140          bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
   4.141      val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts;
   4.142 -    val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
   4.143 +    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
   4.144    in (res, lthy') end;
   4.145  
   4.146  val theorems = gen_theorems (K I) (K I);
   4.147 @@ -389,12 +382,12 @@
   4.148            (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   4.149          |> (fn (res, lthy') =>
   4.150            if Binding.is_empty name andalso null atts then
   4.151 -            (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
   4.152 +            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
   4.153            else
   4.154              let
   4.155                val ([(res_name, _)], lthy'') = lthy'
   4.156                  |> Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])];
   4.157 -              val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
   4.158 +              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
   4.159              in lthy'' end)
   4.160          |> after_qed results'
   4.161        end;
   4.162 @@ -411,7 +404,8 @@
   4.163  
   4.164  in
   4.165  
   4.166 -val theorem = gen_theorem false (K I) Expression.cert_statement;
   4.167 +val theorem' = gen_theorem false (K I) Expression.cert_statement;
   4.168 +fun theorem a b c d e f = theorem' a b c d e f;
   4.169  val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
   4.170  
   4.171  val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;