# HG changeset patch
# User wenzelm
# Date 1303241636 -7200
# Node ID 5b9dd52f5dca6849cf7b5de158dee2748ec1d3b8
# Parent  05f2468d6b3624fbb74ab8e5d611a3215970460d
prefer internal types, via Simple_Syntax.read_typ;

diff -r 05f2468d6b36 -r 5b9dd52f5dca src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Apr 19 21:19:14 2011 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Apr 19 21:33:56 2011 +0200
@@ -32,16 +32,17 @@
 
 (**** tools ****)
 
-fun add_syntax thy =
-  thy
-  |> Theory.copy
-  |> Sign.root_path
-  |> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
-  |> Sign.add_consts
-      [(Binding.name "typeof", "'b::{} => Type", NoSyn),
-       (Binding.name "Type", "'a::{} itself => Type", NoSyn),
-       (Binding.name "Null", "Null", NoSyn),
-       (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
+val typ = Simple_Syntax.read_typ;
+
+val add_syntax =
+  Theory.copy
+  #> Sign.root_path
+  #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
+  #> Sign.add_consts_i
+      [(Binding.name "typeof", typ "'b => Type", NoSyn),
+       (Binding.name "Type", typ "'a itself => Type", NoSyn),
+       (Binding.name "Null", typ "Null", NoSyn),
+       (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)];
 
 val nullT = Type ("Null", []);
 val nullt = Const ("Null", nullT);
@@ -530,7 +531,7 @@
       | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
           let
             val T = etype_of thy' vs Ts prop;
-            val u = if T = nullT then 
+            val u = if T = nullT then
                 (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
               else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
             val (defs', corr_prf) =