# HG changeset patch
# User wenzelm
# Date 1247566244 -7200
# Node ID befec6450fd67b5f6281a9581aead7b797bb60d4
# Parent  1a35de4112bb27dc09754424c15f1c8a36a31b6a
tuned prepare_patternT: Term.exists_subtype;

diff -r 1a35de4112bb -r befec6450fd6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 14 12:10:01 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 14 12:10:44 2009 +0200
@@ -523,16 +523,17 @@
 
 (* patterns *)
 
-fun prepare_patternT ctxt =
-  let val Mode {pattern, schematic, ...} = get_mode ctxt in
-    if pattern orelse schematic then I
-    else Term.map_atyps
-      (fn T as TVar (xi, _) =>
-            if not (TypeInfer.is_param xi)
-            then error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
-            else T
-        | T => T)
-  end;
+fun prepare_patternT ctxt T =
+  let
+    val Mode {pattern, schematic, ...} = get_mode ctxt;
+    val _ =
+      pattern orelse schematic orelse
+        T |> Term.exists_subtype
+          (fn TVar (xi, _) =>
+            not (TypeInfer.is_param xi) andalso
+              error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
+          | _ => false)
+  in T end;
 
 
 local