src/Pure/sign.ML
changeset 24674 4ade7ac6a21c
parent 24517 eaed6ac5f7f2
child 24707 dfeb98f84e93
     1.1 --- a/src/Pure/sign.ML	Sat Sep 22 17:45:55 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Sep 22 17:45:56 2007 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4    val certify_sort: theory -> sort -> sort
     1.5    val certify_typ: theory -> typ -> typ
     1.6    val certify_typ_mode: Type.mode -> theory -> typ -> typ
     1.7 -  val certify': bool -> bool -> Pretty.pp -> Consts.T -> theory -> term -> term * typ * int
     1.8 +  val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
     1.9    val certify_term: theory -> term -> term * typ * int
    1.10    val certify_prop: theory -> term -> term * typ * int
    1.11    val cert_term: theory -> term -> term
    1.12 @@ -437,20 +437,19 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun certify' normalize prop pp consts thy tm =
    1.17 +fun certify' prop pp do_expand consts thy tm =
    1.18    let
    1.19      val _ = check_vars tm;
    1.20      val tm' = Term.map_types (certify_typ thy) tm;
    1.21      val T = type_check pp tm';
    1.22      val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
    1.23 -    val tm'' = Consts.certify pp (tsig_of thy) consts tm';
    1.24 -    val tm'' = if normalize then tm'' else tm';
    1.25 +    val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
    1.26    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
    1.27  
    1.28 -fun certify_term thy = certify' true false (pp thy) (consts_of thy) thy;
    1.29 -fun certify_prop thy = certify' true true (pp thy) (consts_of thy) thy;
    1.30 +fun certify_term thy = certify' false (pp thy) true (consts_of thy) thy;
    1.31 +fun certify_prop thy = certify' true (pp thy) true (consts_of thy) thy;
    1.32  
    1.33 -fun cert_term_abbrev thy = #1 o certify' false false (pp thy) (consts_of thy) thy;
    1.34 +fun cert_term_abbrev thy = #1 o certify' false (pp thy) false (consts_of thy) thy;
    1.35  val cert_term = #1 oo certify_term;
    1.36  val cert_prop = #1 oo certify_prop;
    1.37  
    1.38 @@ -591,7 +590,7 @@
    1.39    let
    1.40      val pp = pp thy;
    1.41      val consts = consts_of thy;
    1.42 -    val cert_consts = Consts.certify pp (tsig_of thy) consts;
    1.43 +    val cert_consts = Consts.certify pp (tsig_of thy) true consts;
    1.44      fun map_free x = if is_some (types (x, ~1)) then SOME x else NONE;
    1.45      val (ts, inst) =
    1.46        read_def_terms' pp (is_logtype thy) (syn_of thy) consts map_free