# HG changeset patch
# User wenzelm
# Date 1267894384 -3600
# Node ID b342390d296f2fe9c07b7ac4bc014be2ab346bfa
# Parent  61bb9f8af129c57b30298552110c778c7d20a7fe
provide ProofContext.def_type depending on "pattern" mode;

diff -r 61bb9f8af129 -r b342390d296f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 06 17:32:45 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 06 17:53:04 2010 +0100
@@ -64,6 +64,7 @@
   val expand_abbrevs: Proof.context -> term -> term
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term
+  val def_type: Proof.context -> indexname -> typ option
   val goal_export: Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
@@ -628,13 +629,15 @@
 
 (* type checking/inference *)
 
+fun def_type ctxt =
+  let val Mode {pattern, ...} = get_mode ctxt
+  in Variable.def_type ctxt pattern end;
+
 fun standard_infer_types ctxt ts =
-  let val Mode {pattern, ...} = get_mode ctxt in
-    TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
-      (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern)
-      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
-    handle TYPE (msg, _, _) => error msg
-  end;
+  TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
+    (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
+    (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
+  handle TYPE (msg, _, _) => error msg;
 
 local