src/Pure/Isar/proof_context.ML

   val strings_of_context: context -> string list
   val print_proof_data: theory -> unit
   val init: theory -> context
   val def_sort: context -> indexname -> sort option
   val def_type: context -> bool -> indexname -> typ option
+  val cert_skolem: context -> string -> string * typ option
   val read_typ: context -> string -> typ
   val cert_typ: context -> typ -> typ
   val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
   val read_term: context -> string -> term
   val read_prop: context -> string -> term

   val read_prop_pat: context -> string -> term
   val cert_term: context -> term -> term
   val cert_prop: context -> term -> term
   val declare_term: term -> context -> context
   val declare_terms: term list -> context -> context
-  val declare_thm: thm -> context -> context
   val add_binds: (indexname * string option) list -> context -> context
   val add_binds_i: (indexname * term option) list -> context -> context
   val match_binds: (string list * string) list -> context -> context
   val match_binds_i: (term list * term) list -> context -> context
   val bind_propp: context * (string * (string list * string list)) -> context * term

     binds: (term * typ) option Vartab.table,                            (*term bindings*)
     thms: thm list option Symtab.table,                                 (*local thms*)
     defs:
       typ Vartab.table *                                                (*type constraints*)
       sort Vartab.table *                                               (*default sorts*)
-      int *                                                             (*maxidx*)
       string list};                                                     (*used type var names*)
 
 exception CONTEXT of string * context;
 
 

   (case prems_of ctxt of
     [] => []
   | prems => [Pretty.string_of (Pretty.big_list "prems:" (map pretty_thm prems))]);
 
 fun strings_of_context (ctxt as Context {asms = (_, (fixes, _)),
-    defs = (types, sorts, maxidx, used), ...}) =
+    defs = (types, sorts, used), ...}) =
   let
     val sign = sign_of ctxt;
 
     val prt_term = Sign.pretty_term sign;
     val prt_typ = Sign.pretty_typ sign;

     strings_of_prems ctxt @
     verb strings_of_binds ctxt @
     verb strings_of_thms ctxt @
     verb_string (Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb_string (Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @
-    verb_string (Pretty.str ("maxidx: " ^ string_of_int maxidx)) @
     verb_string (Pretty.strs ("used type variable names:" :: used))
   end;
 
 
 

 (* init context *)
 
 fun init thy =
   let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
     make_context (thy, data, (([], []), ([], [])), Vartab.empty, Symtab.empty,
-      (Vartab.empty, Vartab.empty, 0, []))
-        (*Note: maxidx = 0 is workaround for obscure bug in Unify.smash_unifiers*)
+      (Vartab.empty, Vartab.empty, []))
   end;
 
 
 (** default sorts and types **)
 
-fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi);
-
-fun def_type (Context {binds, defs = (types, _, _, _), ...}) is_pat xi =
+fun def_sort (Context {defs = (_, sorts, _), ...}) xi = Vartab.lookup (sorts, xi);
+
+fun def_type (Context {binds, defs = (types, _, _), ...}) is_pat xi =
   (case Vartab.lookup (types, xi) of
     None =>
       if is_pat then None
       else (case Vartab.lookup (binds, xi) of Some (Some (_, T)) => Some T | _ => None)
   | some => some);

     if T = propT then t
     else raise TERM ("Term not of type prop", [t])
   end;
 
 
-(* intern_skolem *)
+(* internalize Skolem constants *)
 
 fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);
 
 fun check_skolem ctxt check x =
   if not check then x

           | None => t)
       | intern (t $ u) = intern t $ intern u
       | intern (Abs (x, T, t)) = Abs (x, T, intern t)
       | intern a = a;
   in intern end;
+
+fun cert_skolem ctxt x =
+  (case get_skolem ctxt x of
+    None => raise CONTEXT ("Undeclared variable: " ^ quote x, ctxt)
+  | Some x' => (x', def_type ctxt false (x', ~1)));
 
 
 (* norm_term *)
 
 (*beta normal form for terms (not eta normal form), chase variables in

 end;
 
 
 (* read terms *)
 
-fun gen_read read app is_pat (ctxt as Context {defs = (_, _, _, used), ...}) s =
+fun gen_read read app is_pat (ctxt as Context {defs = (_, _, used), ...}) s =
   (transform_error (read (sign_of ctxt) (def_type ctxt is_pat, def_sort ctxt, used)) s
     handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
     | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   |> app (intern_skolem ctxt true)
   |> app (if is_pat then I else norm_term ctxt)

 fun map_defaults f = map_context
   (fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, thms, f defs));
 
 fun declare (ctxt as Context {asms = (_, (fixes, _)), ...}, t) =
   ctxt
-  |> map_defaults (fn (types, sorts, maxidx, used) => (ins_types (types, t), sorts, maxidx, used))
-  |> map_defaults (fn (types, sorts, maxidx, used) => (types, ins_sorts (sorts, t), maxidx, used))
-  |> map_defaults (fn (types, sorts, maxidx, used) => (types, sorts, maxidx, ins_used (used, t)))
-  |> map_defaults (fn (types, sorts, maxidx, used) =>
-      (types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used))
-  |> map_defaults (fn (types, sorts, maxidx, used) =>
-      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, maxidx, used));
+  |> map_defaults (fn (types, sorts, used) => (ins_types (types, t), sorts, used))
+  |> map_defaults (fn (types, sorts, used) => (types, ins_sorts (sorts, t), used))
+  |> map_defaults (fn (types, sorts, used) => (types, sorts, ins_used (used, t)))
+  |> map_defaults (fn (types, sorts, used) =>
+      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used));
 
 
 fun declare_term t ctxt = declare (ctxt, t);
 fun declare_terms ts ctxt = foldl declare (ctxt, ts);
-
-fun declare_thm thm ctxt =
-  let val {prop, hyps, ...} = Thm.rep_thm thm
-  in ctxt |> declare_terms (prop :: hyps) end;
 
 
 
 (** bindings **)
 

     val t = prep ctxt raw_t;
     val ctxt' = ctxt |> declare_term t;
     val matches = map (fn (f, raw_pat) => (prep_pat ctxt' raw_pat, f t)) raw_pats;
   in (ctxt', (matches, t)) end;
 
+fun maxidx_of_pair (t1, t2) = Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2);
+
 fun gen_match_binds _ [] ctxt = ctxt
   | gen_match_binds prepp args ctxt =
       let
         val raw_pairs = map (apfst (map (pair I))) args;
         val (ctxt', matches) = foldl_map (prep_declare_match prepp) (ctxt, raw_pairs);
         val pairs = flat (map #1 matches);
-        val Context {defs = (_, _, maxidx, _), ...} = ctxt';
+        val maxidx = foldl (fn (i, p) => Int.max (i, maxidx_of_pair p)) (~1, pairs);
         val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs);
         val env =
           (case Seq.pull envs of
             None => raise CONTEXT ("Pattern match failed!", ctxt')
           | Some (env, _) => env);

 local
 
 fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
   let
     val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
-    val Context {defs = (_, _, maxidx, _), ...} = ctxt';
 
     val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
     val cprops_tac = map (rpair tac) cprops;
-    val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops;
+    val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
 
     val ths = map (fn th => ([th], [])) asms;
     val (ctxt'', (_, thms)) =
       ctxt'
       |> auto_bind_facts name props