# HG changeset patch
# User wenzelm
# Date 1007674730 -3600
# Node ID 61e1681b0b5d0eafcde31e4d8ce77030d80e966e
# Parent  f879fcc9412d44d29e941e24b168bb4c6ba01928
added default_type;

diff -r f879fcc9412d -r 61e1681b0b5d src/Pure/Isar/proof_context.ML
--- 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 **)