src/Pure/Isar/specification.ML

 toplevel polymorphism.
 *)
 
 signature SPECIFICATION =
 sig
-  val quiet_mode: bool ref
   val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
   val check_specification: (string * typ option * mixfix) list ->
     ((string * Attrib.src list) * term list) list list -> Proof.context ->
     (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
     Proof.context

   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
     -> local_theory -> (bstring * thm list) list * local_theory
   val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
     -> local_theory -> (bstring * thm list) list * local_theory
-  val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
+  val theorem: string -> Method.text option ->
+    (thm list list -> local_theory -> local_theory) ->
     string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
-  val theorem_cmd: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
+  val theorem_cmd: string -> Method.text option ->
+    (thm list list -> local_theory -> local_theory) ->
     string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
 end;
 

 struct
 
 
 (* diagnostics *)
 
-val quiet_mode = ref false;
-
 fun print_consts _ _ [] = ()
-  | print_consts ctxt pred cs =
-      if ! quiet_mode then () else Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
-
-fun present_results ctxt res =
-  if ! quiet_mode then () else ProofDisplay.present_results ctxt res;
-
-fun present_results' ctxt kind res = present_results ctxt ((kind, ""), res);
+  | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
 
 
 (* prepare specification *)
 
 local

 
 (* axiomatization *)
 
 fun gen_axioms prep raw_vars raw_specs lthy =
   let
-    val (vars, specs) = fst (prep raw_vars [raw_specs] lthy);
-    val cs = map fst vars;
-    val spec_frees = member (op =) ((fold (fold Term.add_frees o snd) specs []));
-
-    val ((constants, axioms), lthy') = lthy
-      |> LocalTheory.consts spec_frees vars
-      ||>> LocalTheory.axioms Thm.axiomK specs;
-    val consts = map #1 constants;
+    val ((vars, specs), _) = prep raw_vars [raw_specs] lthy;
+    val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy;
     val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
-
-    (* FIXME generic target!? *)
-    val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) constants;
-    val lthy'' = lthy' |> LocalTheory.theory (Theory.add_finals_i false hs);
-
-    val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) cs;
-  in ((consts, axioms), lthy'') end;
+    val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
+  in ((consts, axioms), lthy') end;
 
 val axiomatization = gen_axioms check_specification;
 val axiomatization_cmd = gen_axioms read_specification;
 
 

     val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
     val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
       if x = y then mx
       else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     val lthy' = lthy
-      |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
+      |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
       |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
       |> ProofContext.restore_syntax_mode lthy;
 
     val _ = print_consts lthy' (K false) [(x, T)]
   in lthy' end;

     val attrib = prep_att (ProofContext.theory_of lthy);
     val facts = raw_facts |> map (fn ((name, atts), bs) =>
       ((name, map attrib atts),
         bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
     val (res, lthy') = lthy |> LocalTheory.notes kind facts;
-    val _ = present_results' lthy' kind res;
+    val _ = ProofDisplay.present_results lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 val theorems = gen_theorems (K I) (K I);
 val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src;
 

         burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
       in
         lthy
         |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
         |> (fn (res, lthy') =>
-          (present_results lthy' ((kind, name), res);
+          (ProofDisplay.present_results lthy' ((kind, name), res);
             if name = "" andalso null atts then lthy'
             else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
         |> after_qed results'
       end;
   in