removed obsolete IOA/meta_theory/ioa_package.ML;
authorwenzelm
Wed Oct 19 21:52:37 2005 +0200 (2005-10-19)
changeset 1792580a528111a82
parent 17924 75b68d36b787
child 17926 8e12d3a4b890
removed obsolete IOA/meta_theory/ioa_package.ML;
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
     1.1 --- a/src/HOLCF/IOA/ROOT.ML	Wed Oct 19 21:52:36 2005 +0200
     1.2 +++ b/src/HOLCF/IOA/ROOT.ML	Wed Oct 19 21:52:37 2005 +0200
     1.3 @@ -10,4 +10,3 @@
     1.4  
     1.5  time_use_thy "meta_theory/Abstraction";
     1.6  time_use "meta_theory/ioa_package.ML";
     1.7 -time_use "meta_theory/ioa_syn.ML";
     2.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Oct 19 21:52:36 2005 +0200
     2.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Oct 19 21:52:37 2005 +0200
     2.3 @@ -429,15 +429,9 @@
     2.4  end)
     2.5  
     2.6  fun ren_act_type_of thy funct =
     2.7 -let
     2.8 -(* going into a pseudo-proof-state to enable the use of function read *)
     2.9 -val _ = goal thy (funct ^ " = t");
    2.10 -fun arg_typ_of (Type("fun",[a,b])) = a |
    2.11 -arg_typ_of _ = raise malformed;
    2.12 -in
    2.13 -arg_typ_of(#T(rep_cterm(cterm_of (sign_of thy) (read(funct)))))
    2.14 -handle malformed => error ("could not extract argument type of renaming function term")
    2.15 -end;
    2.16 +  (case Term.fastype_of (Sign.read_term thy funct) of
    2.17 +    Type ("fun", [a, b]) => a
    2.18 +  | _ => error "could not extract argument type of renaming function term");
    2.19   
    2.20  fun add_rename automaton_name aut_source fun_name thy =
    2.21  (writeln("Constructing automaton " ^ automaton_name ^ " ...");