src/Pure/Thy/thy_output.ML
changeset 32898 e871d897969c
parent 32890 77df12652210
child 32966 5b21661fe618
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Oct 09 09:14:25 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Oct 09 10:00:47 2009 +0200
     1.3 @@ -443,12 +443,20 @@
     1.4  
     1.5  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
     1.6  
     1.7 -fun pretty_term_abbrev ctxt t = ProofContext.pretty_term_abbrev (Variable.auto_fixes t ctxt) t;
     1.8 +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
     1.9 +
    1.10 +fun pretty_term_style ctxt (style, t) =
    1.11 +  pretty_term ctxt (style t);
    1.12  
    1.13 -fun pretty_term_typ ctxt t =
    1.14 -  Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
    1.15 +fun pretty_thm_style ctxt (style, th) =
    1.16 +  pretty_term ctxt (style (Thm.full_prop_of th));
    1.17  
    1.18 -fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
    1.19 +fun pretty_term_typ ctxt (style, t) =
    1.20 +  let val t' = style t
    1.21 +  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t) end;
    1.22 +
    1.23 +fun pretty_term_typeof ctxt (style, t) =
    1.24 +  Syntax.pretty_typ ctxt (Term.fastype_of (style t));
    1.25  
    1.26  fun pretty_const ctxt c =
    1.27    let
    1.28 @@ -466,15 +474,9 @@
    1.29      val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
    1.30        handle TYPE _ => err ();
    1.31      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
    1.32 -  in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
    1.33 -
    1.34 -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.35 -
    1.36 -fun pretty_term_style ctxt (style, t) =
    1.37 -  pretty_term ctxt (style t);
    1.38 -
    1.39 -fun pretty_thm_style ctxt (style, th) =
    1.40 -  pretty_term_style ctxt (style, Thm.full_prop_of th);
    1.41 +    val eq = Logic.mk_equals (t, t');
    1.42 +    val ctxt' = Variable.auto_fixes eq ctxt;
    1.43 +  in ProofContext.pretty_term_abbrev ctxt' eq end;
    1.44  
    1.45  fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
    1.46  
    1.47 @@ -522,12 +524,10 @@
    1.48  in
    1.49  
    1.50  val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
    1.51 -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
    1.52  val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
    1.53  val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
    1.54 -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
    1.55 -val _ = basic_entity "term_type" Args.term pretty_term_typ;
    1.56 -val _ = basic_entity "typeof" Args.term pretty_term_typeof;
    1.57 +val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
    1.58 +val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
    1.59  val _ = basic_entity "const" Args.const_proper pretty_const;
    1.60  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
    1.61  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
    1.62 @@ -536,6 +536,9 @@
    1.63  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
    1.64  val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
    1.65  
    1.66 +val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
    1.67 +val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
    1.68 +
    1.69  end;
    1.70  
    1.71