src/HOLCF/pcpodef_package.ML
changeset 17325 d9d50222808e
parent 17057 0934ac31985f
child 17336 c05f72cff368
--- a/src/HOLCF/pcpodef_package.ML	Mon Sep 12 17:29:07 2005 +0200
+++ b/src/HOLCF/pcpodef_package.ML	Mon Sep 12 18:20:32 2005 +0200
@@ -79,7 +79,7 @@
       else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
   
     (*lhs*)
-    val lhs_tfrees = map (fn v => (v, getOpt (assoc (rhs_tfrees, v), HOLogic.typeS))) vs;
+    val lhs_tfrees = map (fn v => (v, AList.lookup (op =) rhs_tfrees v |> the_default HOLogic.typeS)) vs;
     val lhs_sorts = map snd lhs_tfrees;
     val tname = Syntax.type_name t mx;
     val full_tname = full tname;