# HG changeset patch
# User wenzelm
# Date 1271338790 -7200
# Node ID 5ca66e58dcfa714ea33a4b7ec8be79a9ce54b35d
# Parent  4ddcc2b07891943683d1f77065c3e235a5f1ee4e
inline old Record.read_typ/cert_typ;
spelling;

diff -r 4ddcc2b07891 -r 5ca66e58dcfa src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Apr 15 15:38:58 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu Apr 15 15:39:50 2010 +0200
@@ -478,6 +478,21 @@
     Type (name, Ts) => (Ts, name)
   | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
 
+fun read_typ ctxt raw_T env =
+  let
+    val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
+    val T = Syntax.read_typ ctxt' raw_T;
+    val env' = OldTerm.add_typ_tfrees (T, env);
+  in (T, env') end;
+
+fun cert_typ ctxt raw_T env =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val T = Type.no_tvars (Sign.certify_typ thy raw_T)
+      handle TYPE (msg, _, _) => error msg;
+    val env' = OldTerm.add_typ_tfrees (T, env);
+  in (T, env') end;
+
 fun gen_define_statespace prep_typ state_space args name parents comps thy =
   let (* - args distinct
          - only args may occur in comps and parent-instantiations
@@ -500,7 +515,7 @@
 
         val (Ts',env') = fold_map (prep_typ ctxt) Ts env
             handle ERROR msg => cat_error msg
-                    ("The error(s) above occured in parent statespace specification "
+                    ("The error(s) above occurred in parent statespace specification "
                     ^ quote pname);
         val err_insts = if length args <> length Ts' then
             ["number of type instantiation(s) does not match arguments of parent statespace "
@@ -539,7 +554,7 @@
 
     fun prep_comp (n,T) env =
       let val (T', env') = prep_typ ctxt T env handle ERROR msg =>
-       cat_error msg ("The error(s) above occured in component " ^ quote n)
+       cat_error msg ("The error(s) above occurred in component " ^ quote n)
       in ((n,T'), env') end;
 
     val (comps',env') = fold_map prep_comp comps env;
@@ -579,8 +594,8 @@
   end
   handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
 
-val define_statespace = gen_define_statespace Record.read_typ NONE;
-val define_statespace_i = gen_define_statespace Record.cert_typ;
+val define_statespace = gen_define_statespace read_typ NONE;
+val define_statespace_i = gen_define_statespace cert_typ;
 
 
 (*** parse/print - translations ***)