diff -r 50ea65e84d98 -r b1965c8992c8 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Tools/Code/code_preproc.ML Mon Apr 18 13:26:39 2011 +0200 @@ -431,8 +431,7 @@ |> fold (ensure_fun thy arities eqngr) cs |> fold (ensure_rhs thy arities eqngr) cs_rhss; val arities' = fold (add_arity thy vardeps) insts arities; - val pp = Context.pretty_global thy; - val algebra = Sorts.subalgebra pp (is_proper_class thy) + val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy) (AList.lookup (op =) arities') (Sign.classes_of thy); val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr); fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)