# HG changeset patch
# User wenzelm
# Date 1129751557 -7200
# Node ID 80a528111a82df183ea54f645f9241f77ba55e7e
# Parent  75b68d36b787434e882a113b760c2b45127e173f
removed obsolete IOA/meta_theory/ioa_package.ML;

diff -r 75b68d36b787 -r 80a528111a82 src/HOLCF/IOA/ROOT.ML
--- a/src/HOLCF/IOA/ROOT.ML	Wed Oct 19 21:52:36 2005 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Wed Oct 19 21:52:37 2005 +0200
@@ -10,4 +10,3 @@
 
 time_use_thy "meta_theory/Abstraction";
 time_use "meta_theory/ioa_package.ML";
-time_use "meta_theory/ioa_syn.ML";
diff -r 75b68d36b787 -r 80a528111a82 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Oct 19 21:52:36 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Oct 19 21:52:37 2005 +0200
@@ -429,15 +429,9 @@
 end)
 
 fun ren_act_type_of thy funct =
-let
-(* going into a pseudo-proof-state to enable the use of function read *)
-val _ = goal thy (funct ^ " = t");
-fun arg_typ_of (Type("fun",[a,b])) = a |
-arg_typ_of _ = raise malformed;
-in
-arg_typ_of(#T(rep_cterm(cterm_of (sign_of thy) (read(funct)))))
-handle malformed => error ("could not extract argument type of renaming function term")
-end;
+  (case Term.fastype_of (Sign.read_term thy funct) of
+    Type ("fun", [a, b]) => a
+  | _ => error "could not extract argument type of renaming function term");
  
 fun add_rename automaton_name aut_source fun_name thy =
 (writeln("Constructing automaton " ^ automaton_name ^ " ...");