# HG changeset patch
# User krauss
# Date 1227556803 -3600
# Node ID 0f5b1accfb94c46d7e0e54c9928ea98c80a9b120
# Parent  57bfd0fdea0956f974448da672b8c9acf45bf14e
improved error msg; tuned

diff -r 57bfd0fdea09 -r 0f5b1accfb94 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 24 20:12:23 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 24 21:00:03 2008 +0100
@@ -107,7 +107,8 @@
     let 
       val term = Drule.term_rule thy f
     in
-      Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term)
+      Morphism.thm_morphism f $> Morphism.term_morphism term 
+       $> Morphism.typ_morphism (Logic.type_map term)
     end
 
 fun import_fundef_data t ctxt =
@@ -189,7 +190,8 @@
     FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
 
 val default_config =
-  FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false }
+  FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
+                 domintros=false, tailrec=false }
 
 
 (* Analyzing function equations *)
@@ -234,43 +236,51 @@
                                 
       fun check geq = 
           let
-            fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
+            fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt 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 
-                                               ^ commas_quote fnames))
+                    orelse input_error 
+                             ("Head symbol of left hand side must be " 
+                              ^ plural "" "one out of " fnames ^ commas_quote fnames)
                                             
             fun add_bvs t is = add_loose_bnos (t, 0, is)
             val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
                         |> map (fst o nth (rev qs))
                       
-            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
-                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
+            val _ = null rvs orelse input_error 
+                        ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
+                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
                                     
-            val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs 
-                    orelse error (input_error "Recursive Calls not allowed in premises")
+            val _ = forall (not o Term.exists_subterm 
+                             (fn Free (n, _) => n mem fnames | _ => false)) gs 
+                    orelse input_error "Recursive Calls not allowed in premises"
 
             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 _ = null funvars
-                    orelse (warning (cat_lines ["Bound variable" ^ plural " " "s " funvars ^ commas_quote (map fst funvars) ^  
-                                                " occur" ^ plural "s" "" funvars ^ " in function position.",  
-                                                "Misspelled constructor???"]); true)
+                    orelse (warning (cat_lines 
+                    ["Bound variable" ^ plural " " "s " funvars 
+                     ^ commas_quote (map fst funvars) ^  
+                     " occur" ^ plural "s" "" funvars ^ " in function position.",  
+                     "Misspelled constructor???"]); true)
           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" ^ ".")
+          orelse error (cat_lines 
+          ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
+           setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
 
       val _ = map check_sorts fixes
 
       val _ = mk_arities (map check eqs)
           handle ArgumentCount fname => 
-                 error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
+                 error ("Function " ^ quote fname ^ 
+                        " has different numbers of arguments in different equations")
     in
       ()
     end
@@ -282,7 +292,8 @@
 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec 
                -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
 
-val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
+val fname_of = fst o dest_Free o fst o strip_comb o fst 
+ o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
 
 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   | mk_case_names _ n 0 = []
@@ -297,7 +308,8 @@
       val fnames = map (fst o fst) fixes
       val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
 
-      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
+      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
+                                   (indices ~~ xs)
                         |> map (map snd)
 
       (* using theorem names for case name currently disabled *)
@@ -322,27 +334,32 @@
 local 
   structure P = OuterParse and K = OuterKeyword
 
-  val option_parser = (P.reserved "sequential" >> K Sequential)
-                   || ((P.reserved "default" |-- P.term) >> Default)
-                   || (P.reserved "domintros" >> K DomIntros)
-                   || (P.reserved "tailrec" >> K Tailrec)
+  val option_parser = 
+      P.group "option" ((P.reserved "sequential" >> K Sequential)
+                    || ((P.reserved "default" |-- P.term) >> Default)
+                    || (P.reserved "domintros" >> K DomIntros)
+                    || (P.reserved "tailrec" >> K Tailrec))
 
-  fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
-                              >> (fn opts => fold apply_opt opts default)
+  fun config_parser default = 
+      (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+        >> (fn opts => fold apply_opt opts default)
 
   val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
 
-  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
+  fun pipe_error t = 
+  P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
 
-  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
-                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
+  val statement_ow = 
+   SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
+    --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
 
   val statements_ow = P.enum1 "|" statement_ow
 
   val flags_statements = statements_ow
                          >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
 in
-  fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
+  fun fundef_parser default_cfg = 
+      config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements
 end