added no_frees;
authorwenzelm
Sun Dec 10 15:30:39 2006 +0100 (2006-12-10)
changeset 217415f3d62008bb5
parent 21740 2982e6ae2a2f
child 21742 a330e58226d0
added no_frees;
add_abbrev: tuned handling of frees, temp workaround;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sun Dec 10 15:30:38 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Dec 10 15:30:39 2006 +0100
     1.3 @@ -157,6 +157,7 @@
     1.4    val certify_prop: theory -> term -> term * typ * int
     1.5    val cert_term: theory -> term -> term
     1.6    val cert_prop: theory -> term -> term
     1.7 +  val no_frees: Pretty.pp -> term -> term
     1.8    val no_vars: Pretty.pp -> term -> term
     1.9    val cert_def: Pretty.pp -> term -> (string * typ) * term
    1.10    val read_class: theory -> xstring -> class
    1.11 @@ -482,12 +483,15 @@
    1.12  
    1.13  (* specifications *)
    1.14  
    1.15 -fun no_vars pp tm =
    1.16 -  (case (Term.add_vars tm [], Term.add_tvars tm []) of
    1.17 +fun no_variables kind add addT mk mkT pp tm =
    1.18 +  (case (add tm [], addT tm []) of
    1.19      ([], []) => tm
    1.20 -  | (vars, tvars) => error (Pretty.string_of (Pretty.block (Pretty.breaks
    1.21 -      (Pretty.str "Illegal schematic variable(s) in term:" ::
    1.22 -       map (Pretty.term pp o Var) vars @ map (Pretty.typ pp o TVar) tvars)))));
    1.23 +  | (frees, tfrees) => error (Pretty.string_of (Pretty.block (Pretty.breaks
    1.24 +      (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") ::
    1.25 +       map (Pretty.term pp o mk) frees @ map (Pretty.typ pp o mkT) tfrees)))));
    1.26 +
    1.27 +val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
    1.28 +val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
    1.29  
    1.30  fun cert_def pp tm =
    1.31    let val ((lhs, rhs), _) = tm
    1.32 @@ -754,11 +758,14 @@
    1.33  
    1.34  fun add_abbrev mode (c, raw_t) thy =
    1.35    let
    1.36 -    val prep_tm = Compress.term thy o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.37 +    val pp = pp thy;
    1.38 +    val prep_tm = Compress.term thy o no_frees pp o
    1.39 +      map_types Logic.legacy_varifyT (* FIXME tmp *) o
    1.40 +      Term.no_dummy_patterns o cert_term_abbrev thy;
    1.41      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.42        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    1.43      val (res, consts') = consts_of thy
    1.44 -      |> Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode (c, t);
    1.45 +      |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode (c, t);
    1.46    in (res, thy |> map_consts (K consts')) end;
    1.47  
    1.48