--- a/src/Pure/Isar/proof_context.ML Thu Dec 06 17:16:46 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Dec 06 22:38:50 2001 +0100
@@ -20,6 +20,7 @@
val print_proof_data: theory -> unit
val init: theory -> context
val is_fixed: context -> string -> bool
+ val default_type: context -> string -> typ option
val read_typ: context -> string -> typ
val read_typ_no_norm: context -> string -> typ
val cert_typ: context -> typ -> typ
@@ -387,6 +388,9 @@
| _ => None)
| some => some);
+fun default_type (Context {binds, defs = (types, _, _, _), ...}) x =
+ Vartab.lookup (types, (x, ~1));
+
(** prepare types **)