eliminated Syntax.binding;
authorwenzelm
Sat Sep 04 21:12:15 1999 +0200 (1999-09-04)
changeset 7479b482d827899c
parent 7478 02291239d627
child 7480 0a0e0dbe1269
eliminated Syntax.binding;
put_thms: ignore "";
update_binds_env: Envir.norm_term ensures proper type instantiation;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Sep 04 21:08:38 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Sep 04 21:12:15 1999 +0200
     1.3 @@ -134,13 +134,7 @@
     1.4  fun strings_of_binds (Context {thy, binds, ...}) =
     1.5    let
     1.6      val prt_term = Sign.pretty_term (Theory.sign_of thy);
     1.7 -
     1.8 -    fun fix_var (x, i) =
     1.9 -      (case try Syntax.dest_binding x of
    1.10 -        None => Syntax.string_of_vname (x, i)
    1.11 -      | Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
    1.12 -    fun pretty_bind (xi, (t, T)) = Pretty.block
    1.13 -      [Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
    1.14 +    fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t));
    1.15    in
    1.16      if Vartab.is_empty binds andalso not (! verbose) then []
    1.17      else [Pretty.string_of (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds)))]
    1.18 @@ -394,10 +388,7 @@
    1.19              Some (u, U) =>
    1.20                if T = U then (norm u handle SAME => u)
    1.21                else raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u])
    1.22 -          | None =>
    1.23 -              if can Syntax.dest_binding (#1 xi) then
    1.24 -                raise CONTEXT ("Unbound binding: " ^ Syntax.string_of_vname xi, ctxt)
    1.25 -              else raise SAME)
    1.26 +          | None => raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt))
    1.27        | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
    1.28        | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
    1.29        | norm (f $ t) =
    1.30 @@ -432,10 +423,6 @@
    1.31  
    1.32  (* read terms *)
    1.33  
    1.34 -fun warn_vars ctxt tm =
    1.35 -  if null (term_vars tm) andalso null (term_tvars tm) then tm
    1.36 -  else (warning "Illegal schematic variable(s) in term"; tm);
    1.37 -
    1.38  fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
    1.39    let
    1.40      val sign = sign_of ctxt;
    1.41 @@ -453,7 +440,6 @@
    1.42      |> app (intern_skolem ctxt true)
    1.43      |> app (if is_pat then I else norm_term ctxt)
    1.44      |> app (if is_pat then prepare_dummies else (reject_dummies ctxt))
    1.45 -    |> app (if is_pat then I else warn_vars ctxt)
    1.46    end;
    1.47  
    1.48  val read_termTs = gen_read (read_def_termTs false) (apfst o map) false;
    1.49 @@ -535,17 +521,14 @@
    1.50    end;
    1.51  
    1.52  fun update_binds bs ctxt = foldl upd_bind (ctxt, bs);
    1.53 -fun update_binds_env env = update_binds (Envir.alist_of env);
    1.54 +fun update_binds_env env = (*Envir.norm_term ensures proper type instantiation*)
    1.55 +  update_binds (map (apsnd (Envir.norm_term env)) (Envir.alist_of env));
    1.56  
    1.57  
    1.58  (* add_binds(_i) -- sequential *)
    1.59  
    1.60  fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) =
    1.61 -  let val t = prep ctxt raw_t in
    1.62 -    if can Syntax.dest_binding x then ctxt |> update_binds [(xi, t)]
    1.63 -    else raise CONTEXT ("Illegal variable name for term binding: " ^
    1.64 -      quote (Syntax.string_of_vname xi), ctxt)
    1.65 -  end;
    1.66 +  ctxt |> update_binds [(xi, prep ctxt raw_t)];
    1.67  
    1.68  fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds);
    1.69  
    1.70 @@ -632,9 +615,10 @@
    1.71  
    1.72  (* put_thm(s) *)
    1.73  
    1.74 -fun put_thms (name, ths) = map_context
    1.75 -  (fn (thy, data, asms, binds, thms, defs) =>
    1.76 -    (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
    1.77 +fun put_thms ("", _) = I
    1.78 +  | put_thms (name, ths) = map_context
    1.79 +      (fn (thy, data, asms, binds, thms, defs) =>
    1.80 +        (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
    1.81  
    1.82  fun put_thm (name, th) = put_thms (name, [th]);
    1.83