src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 17925 80a528111a82
parent 17243 c4ff384ee28f
child 18358 0a733e11021a
     1.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Oct 19 21:52:36 2005 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Oct 19 21:52:37 2005 +0200
     1.3 @@ -429,15 +429,9 @@
     1.4  end)
     1.5  
     1.6  fun ren_act_type_of thy funct =
     1.7 -let
     1.8 -(* going into a pseudo-proof-state to enable the use of function read *)
     1.9 -val _ = goal thy (funct ^ " = t");
    1.10 -fun arg_typ_of (Type("fun",[a,b])) = a |
    1.11 -arg_typ_of _ = raise malformed;
    1.12 -in
    1.13 -arg_typ_of(#T(rep_cterm(cterm_of (sign_of thy) (read(funct)))))
    1.14 -handle malformed => error ("could not extract argument type of renaming function term")
    1.15 -end;
    1.16 +  (case Term.fastype_of (Sign.read_term thy funct) of
    1.17 +    Type ("fun", [a, b]) => a
    1.18 +  | _ => error "could not extract argument type of renaming function term");
    1.19   
    1.20  fun add_rename automaton_name aut_source fun_name thy =
    1.21  (writeln("Constructing automaton " ^ automaton_name ^ " ...");