--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Feb 13 17:15:14 2005 +0100
@@ -98,7 +98,7 @@
fun unqualify s = implode(rev(afpl(rev(explode s))));
val q_atypstr = act_name thy atyp;
val uq_atypstr = unqualify q_atypstr;
-val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct", None));
+val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct", NONE));
in
extract_constrs thy prem
handle malformed =>
@@ -284,7 +284,7 @@
let
fun left_of (( _ $ left) $ _) = left |
left_of _ = raise malformed;
-val aut_def = concl_of (get_thm thy (aut_name ^ "_def", None));
+val aut_def = concl_of (get_thm thy (aut_name ^ "_def", NONE));
in
(#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def))))
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")