more error handling

--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Aug 07 15:04:35 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Aug 07 15:20:24 2007 +0200
@@ -173,22 +173,21 @@
 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
   | open_all_all t = ([], t)
 
-exception MalformedEquation of term
-
-fun split_def geq =
+fun split_def ctxt geq =
     let
+      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
       val (qs, imp) = open_all_all geq
 
       val gs = Logic.strip_imp_prems imp
       val eq = Logic.strip_imp_concl imp
 
       val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
-          handle TERM _ => raise MalformedEquation geq
+          handle TERM _ => error (input_error "Not an equation")
 
       val (head, args) = strip_comb f_args
 
       val fname = fst (dest_Free head)
-          handle TERM _ => raise MalformedEquation geq
+          handle TERM _ => error (input_error "Head symbol must not be a bound variable")
     in
       (fname, qs, gs, args, rhs)
     end
@@ -217,7 +216,7 @@
           let
             fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
                                   
-            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
+            val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
                                  
             val _ = fname mem fnames 
                     orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
@@ -235,6 +234,12 @@
           in
             fqgar
           end
+          
+      fun check_sorts ((fname, fT), _) =
+          Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+          orelse error ("Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ".")
+
+      val _ = map check_sorts fixes
 
       val _ = mk_arities (map check eqs)
           handle ArgumentCount fname => 

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Aug 07 15:04:35 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Aug 07 15:20:24 2007 +0200
@@ -41,13 +41,13 @@
              ())
           end
           
-      val (fname, qs, gs, args, rhs) = split_def geq 
+      val (fname, qs, gs, args, rhs) = split_def ctxt geq 
                                        
       val _ = if not (null gs) then err "Conditional equations" else ()
       val _ = map check_constr_pattern args
                   
                   (* just count occurrences to check linearity *)
-      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 < length qs
+      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs
               then err "Nonlinear patterns" else ()
     in
       ()
@@ -226,9 +226,9 @@
       map mk_eqn fixes
     end
 
-fun add_catchall fixes spec =
+fun add_catchall ctxt fixes spec =
     let 
-      val catchalls = mk_catchall fixes (mk_arities (map split_def (map snd spec)))
+      val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec)))
     in
       spec @ map (pair true) catchalls
     end
@@ -249,7 +249,7 @@
                            |> tap (check_defs ctxt fixes) (* Standard checks *)
                            |> tap (map (check_pats ctxt))    (* More checks for sequential mode *)
                            |> curry op ~~ flags'
-                           |> add_catchall fixes   (* Completion *)
+                           |> add_catchall ctxt fixes   (* Completion *)
                            |> FundefSplit.split_some_equations ctxt
 
           fun restore_spec thms =

--- a/src/HOL/Tools/function_package/mutual.ML	Tue Aug 07 15:04:35 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Aug 07 15:20:24 2007 +0200
@@ -121,7 +121,7 @@
     let
       val num = length fs
         val fnames = map fst fs
-        val fqgars = map split_def eqs
+        val fqgars = map (split_def ctxt) eqs
         val arities = mk_arities fqgars
 
         fun curried_types (fname, fT) =