fixed declatation of patterns and skolem;
authorwenzelm
Sun Nov 29 13:21:38 1998 +0100 (1998-11-29)
changeset 59947b84677315ed
parent 5993 d03fbef54c62
child 5995 450cd1f0270b
fixed declatation of patterns and skolem;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 29 13:20:49 1998 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 29 13:21:38 1998 +0100
     1.3 @@ -439,16 +439,24 @@
     1.4      | (used, TVar ((x, _), _)) => x ins used
     1.5      | (used, _) => used));
     1.6  
     1.7 +fun ins_skolem def_type = foldr
     1.8 +  (fn ((x, x'), types) =>
     1.9 +    (case def_type x' of
    1.10 +      Some T => Vartab.update (((x, ~1), T), types)
    1.11 +    | None => types));
    1.12 +
    1.13  fun map_defaults f = map_context
    1.14    (fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, thms, f defs));
    1.15  
    1.16 -fun declare (ctxt, t) =
    1.17 +fun declare (ctxt as Context {asms = (_, (fixes, _)), ...}, t) =
    1.18    ctxt
    1.19    |> map_defaults (fn (types, sorts, maxidx, used) => (ins_types (types, t), sorts, maxidx, used))
    1.20    |> map_defaults (fn (types, sorts, maxidx, used) => (types, ins_sorts (sorts, t), maxidx, used))
    1.21    |> map_defaults (fn (types, sorts, maxidx, used) => (types, sorts, maxidx, ins_used (used, t)))
    1.22    |> map_defaults (fn (types, sorts, maxidx, used) =>
    1.23 -      (types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used));
    1.24 +      (types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used))
    1.25 +  |> map_defaults (fn (types, sorts, maxidx, used) =>
    1.26 +      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, maxidx, used));
    1.27  
    1.28  
    1.29  fun declare_term t ctxt = declare (ctxt, t);
    1.30 @@ -495,9 +503,10 @@
    1.31  
    1.32  fun prep_declare_match (prep_pat, prep) (ctxt, (raw_pats, raw_t)) =
    1.33    let
    1.34 -    val pats = map (prep_pat ctxt) raw_pats;		(* FIXME seq / par / simult (??) *)
    1.35      val t = prep ctxt raw_t;
    1.36 -  in (ctxt |> declare_term t, (map (rpair t) pats, t)) end;
    1.37 +    val ctxt' = ctxt |> declare_term t;
    1.38 +    val pats = map (prep_pat ctxt') raw_pats;		(* FIXME seq / par / simult (??) *)
    1.39 +  in (ctxt', (map (rpair t) pats, t)) end;
    1.40  
    1.41  fun gen_match_binds _ [] ctxt = ctxt
    1.42    | gen_match_binds prepp raw_pairs ctxt =