diff -r 2eeb75cccb8d -r 25a7f421a3ba Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Thu Jun 16 11:03:01 2011 +0100
+++ b/Nominal/nominal_function.ML	Thu Jun 16 12:12:25 2011 +0100
@@ -45,6 +45,8 @@
 (* Check for all sorts of errors in the input - nominal needs a different checking function *)
 fun nominal_check_defs ctxt fixes eqs =
   let
+    val _ = tracing ("fixes: " ^ @{make_string} fixes)
+
     val fnames = map (fst o fst) fixes
 
     fun check geq =
@@ -68,7 +70,8 @@
           orelse input_error "Defined function may not occur in premises or arguments"
 
         val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
-        val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
+        val funvars = filter (fn q => 
+          exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
         val _ = null funvars orelse (warning (cat_lines
           ["Bound variable" ^ plural " " "s " funvars ^
           commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^
@@ -90,9 +93,9 @@
         plural " " "s " not_defined ^ commas_quote not_defined)
 
     fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+      Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, @{sort "pt"})
       orelse error (cat_lines
-      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
+      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "pt" ^ ":",
        Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
 
     val _ = map check_sorts fixes
@@ -144,11 +147,7 @@
       empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *)
 
     val defname = mk_defname fixes
-    val NominalFunctionConfig {partials, default, ...} = config
-    val _ =
-      if is_some default then Output.legacy_feature
-        "'function (default)'. Use 'partial_function'."
-      else ()
+    val NominalFunctionConfig {partials, ...} = config
 
     val ((goal_state, cont), lthy') =
       Nominal_Function_Mutual.prepare_nominal_function_mutual config defname fixes eqs lthy