src/Pure/Isar/specification.ML
changeset 26595 855893d4d75f
parent 26345 f70620a4cf81
child 27858 d385b67f8439
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Apr 09 21:49:36 2008 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Apr 09 21:49:37 2008 +0200
     1.3 @@ -142,21 +142,23 @@
     1.4  
     1.5  (* axiomatization *)
     1.6  
     1.7 -fun gen_axioms prep raw_vars raw_specs lthy =
     1.8 +fun gen_axioms do_print prep raw_vars raw_specs lthy =
     1.9    let
    1.10      val ((vars, specs), _) = prep raw_vars [raw_specs] lthy;
    1.11      val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy;
    1.12      val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
    1.13 -    val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
    1.14 +    val _ =
    1.15 +      if not do_print then ()
    1.16 +      else print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
    1.17    in ((consts, axioms), lthy') end;
    1.18  
    1.19 -val axiomatization = gen_axioms check_specification;
    1.20 -val axiomatization_cmd = gen_axioms read_specification;
    1.21 +val axiomatization = gen_axioms false check_specification;
    1.22 +val axiomatization_cmd = gen_axioms true read_specification;
    1.23  
    1.24  
    1.25  (* definition *)
    1.26  
    1.27 -fun gen_def prep (raw_var, (raw_a, raw_prop)) lthy =
    1.28 +fun gen_def do_print prep (raw_var, (raw_a, raw_prop)) lthy =
    1.29    let
    1.30      val (vars, [((raw_name, atts), [prop])]) =
    1.31        fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
    1.32 @@ -172,16 +174,18 @@
    1.33            ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
    1.34  
    1.35      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
    1.36 -    val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    1.37 +    val _ =
    1.38 +      if not do_print then ()
    1.39 +      else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    1.40    in ((lhs, (b, th')), lthy3) end;
    1.41  
    1.42 -val definition = gen_def check_free_specification;
    1.43 -val definition_cmd = gen_def read_free_specification;
    1.44 +val definition = gen_def false check_free_specification;
    1.45 +val definition_cmd = gen_def true read_free_specification;
    1.46  
    1.47  
    1.48  (* abbreviation *)
    1.49  
    1.50 -fun gen_abbrev prep mode (raw_var, raw_prop) lthy =
    1.51 +fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
    1.52    let
    1.53      val ((vars, [(_, [prop])]), _) =
    1.54        prep (the_list raw_var) [(("", []), [raw_prop])]
    1.55 @@ -195,11 +199,11 @@
    1.56        |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
    1.57        |> ProofContext.restore_syntax_mode lthy;
    1.58  
    1.59 -    val _ = print_consts lthy' (K false) [(x, T)]
    1.60 +    val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
    1.61    in lthy' end;
    1.62  
    1.63 -val abbreviation = gen_abbrev check_free_specification;
    1.64 -val abbreviation_cmd = gen_abbrev read_free_specification;
    1.65 +val abbreviation = gen_abbrev false check_free_specification;
    1.66 +val abbreviation_cmd = gen_abbrev true read_free_specification;
    1.67  
    1.68  
    1.69  (* notation *)