--- a/Nominal/nominal_function.ML	Thu Sep 22 11:42:55 2011 +0200
+++ b/Nominal/nominal_function.ML	Thu Nov 03 13:19:23 2011 +0000
@@ -91,7 +91,7 @@
         plural " " "s " not_defined ^ commas_quote not_defined)
 
     fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, @{sort "pt"})
+      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort "pt"})
       orelse error (cat_lines
       ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":",
        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
@@ -184,7 +184,8 @@
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info, 
-         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
+         lthy |> Local_Theory.declaration {syntax = false, pervasive = false} 
+           (add_function_data o morph_function_data info))
       end
   in
     ((goal_state, afterqed), lthy')