src/Pure/Isar/class_target.ML
changeset 35669 a91c7ed801b8
parent 35315 fbdc860d87a3
child 35845 e5980f0ad025
--- a/src/Pure/Isar/class_target.ML	Tue Mar 09 14:29:47 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Tue Mar 09 14:35:02 2010 +0100
@@ -417,7 +417,8 @@
 
 fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   let
-    val all_arities = map (fn raw_tyco => Sign.read_arity thy
+    val ctxt = ProofContext.init thy;
+    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
       (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
     val tycos = map #1 all_arities;
     val (_, sorts, sort) = hd all_arities;