removed unused/impure quiet_mode;
authorwenzelm
Thu Oct 11 21:10:42 2007 +0200 (2007-10-11)
changeset 249861f902ded7f70
parent 24985 0e5177e2c076
child 24987 50b07326da38
removed unused/impure quiet_mode;
local_theory: incorporated consts into axioms;
tuned;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Oct 11 21:10:41 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Oct 11 21:10:42 2007 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  signature SPECIFICATION =
     1.6  sig
     1.7 -  val quiet_mode: bool ref
     1.8    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
     1.9    val check_specification: (string * typ option * mixfix) list ->
    1.10      ((string * Attrib.src list) * term list) list list -> Proof.context ->
    1.11 @@ -48,10 +47,12 @@
    1.12      -> local_theory -> (bstring * thm list) list * local_theory
    1.13    val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.14      -> local_theory -> (bstring * thm list) list * local_theory
    1.15 -  val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    1.16 +  val theorem: string -> Method.text option ->
    1.17 +    (thm list list -> local_theory -> local_theory) ->
    1.18      string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
    1.19      bool -> local_theory -> Proof.state
    1.20 -  val theorem_cmd: string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    1.21 +  val theorem_cmd: string -> Method.text option ->
    1.22 +    (thm list list -> local_theory -> local_theory) ->
    1.23      string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
    1.24      bool -> local_theory -> Proof.state
    1.25    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    1.26 @@ -63,16 +64,8 @@
    1.27  
    1.28  (* diagnostics *)
    1.29  
    1.30 -val quiet_mode = ref false;
    1.31 -
    1.32  fun print_consts _ _ [] = ()
    1.33 -  | print_consts ctxt pred cs =
    1.34 -      if ! quiet_mode then () else Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
    1.35 -
    1.36 -fun present_results ctxt res =
    1.37 -  if ! quiet_mode then () else ProofDisplay.present_results ctxt res;
    1.38 -
    1.39 -fun present_results' ctxt kind res = present_results ctxt ((kind, ""), res);
    1.40 +  | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
    1.41  
    1.42  
    1.43  (* prepare specification *)
    1.44 @@ -150,22 +143,11 @@
    1.45  
    1.46  fun gen_axioms prep raw_vars raw_specs lthy =
    1.47    let
    1.48 -    val (vars, specs) = fst (prep raw_vars [raw_specs] lthy);
    1.49 -    val cs = map fst vars;
    1.50 -    val spec_frees = member (op =) ((fold (fold Term.add_frees o snd) specs []));
    1.51 -
    1.52 -    val ((constants, axioms), lthy') = lthy
    1.53 -      |> LocalTheory.consts spec_frees vars
    1.54 -      ||>> LocalTheory.axioms Thm.axiomK specs;
    1.55 -    val consts = map #1 constants;
    1.56 +    val ((vars, specs), _) = prep raw_vars [raw_specs] lthy;
    1.57 +    val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy;
    1.58      val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
    1.59 -
    1.60 -    (* FIXME generic target!? *)
    1.61 -    val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) constants;
    1.62 -    val lthy'' = lthy' |> LocalTheory.theory (Theory.add_finals_i false hs);
    1.63 -
    1.64 -    val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) cs;
    1.65 -  in ((consts, axioms), lthy'') end;
    1.66 +    val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
    1.67 +  in ((consts, axioms), lthy') end;
    1.68  
    1.69  val axiomatization = gen_axioms check_specification;
    1.70  val axiomatization_cmd = gen_axioms read_specification;
    1.71 @@ -208,7 +190,7 @@
    1.72        if x = y then mx
    1.73        else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
    1.74      val lthy' = lthy
    1.75 -      |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
    1.76 +      |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
    1.77        |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
    1.78        |> ProofContext.restore_syntax_mode lthy;
    1.79  
    1.80 @@ -237,7 +219,7 @@
    1.81        ((name, map attrib atts),
    1.82          bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts))));
    1.83      val (res, lthy') = lthy |> LocalTheory.notes kind facts;
    1.84 -    val _ = present_results' lthy' kind res;
    1.85 +    val _ = ProofDisplay.present_results lthy' ((kind, ""), res);
    1.86    in (res, lthy') end;
    1.87  
    1.88  val theorems = gen_theorems (K I) (K I);
    1.89 @@ -335,7 +317,7 @@
    1.90          lthy
    1.91          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    1.92          |> (fn (res, lthy') =>
    1.93 -          (present_results lthy' ((kind, name), res);
    1.94 +          (ProofDisplay.present_results lthy' ((kind, name), res);
    1.95              if name = "" andalso null atts then lthy'
    1.96              else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
    1.97          |> after_qed results'