# HG changeset patch
# User berghofe
# Date 1015499023 -3600
# Node ID e968745986f11bc4f210f0309bbfc902454b3f44
# Parent  f7f29f8380ceb5df81da6042abae4512fd411581
- made modes_of more robust
- assoc_code now has higher priority than inductive_codegen

diff -r f7f29f8380ce -r e968745986f1 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Mar 06 23:59:28 2002 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Mar 07 12:03:43 2002 +0100
@@ -127,6 +127,10 @@
 val term_vs = map (fst o fst o dest_Var) o term_vars;
 val terms_vs = distinct o flat o (map term_vs);
 
+fun assoc' s tab key = (case assoc (tab, key) of
+      None => error ("Unable to determine " ^ s ^ " of " ^ quote key)
+    | Some x => x);
+
 (** collect all Vars in a term (with duplicates!) **)
 fun term_vTs t = map (apfst fst o dest_Var)
   (filter is_Var (foldl_aterms (op :: o Library.swap) ([], t)));
@@ -163,11 +167,12 @@
         (fn (None, _) => [None]
           | (Some js, arg) => map Some
               (filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
-                (iss ~~ args)))) (the (assoc (modes, name))))
+                (iss ~~ args)))) (assoc' "modes" modes name))
 
   in (case strip_comb t of
       (Const (name, _), args) => mk_modes name args
-    | (Var ((name, _), _), args) => mk_modes name args)
+    | (Var ((name, _), _), args) => mk_modes name args
+    | (Free (name, _), args) => mk_modes name args)
   end;
 
 datatype indprem = Prem of term list * term | Sidecond of term;
@@ -478,9 +483,9 @@
   end;
 
 fun mk_ind_call thy gr dep t u is_query = (case head_of u of
-  Const (s, _) => (case get_clauses thy s of
-       None => None
-     | Some (names, intrs) =>
+  Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
+       (None, _) => None
+     | (Some (names, intrs), None) =>
          let
           fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
                 ((ts, mode), i+1)
@@ -504,7 +509,8 @@
          in
            Some (gr3, Pretty.block
              (ps @ [Pretty.brk 1, mk_tuple in_ps]))
-         end)
+         end
+     | _ => None)
   | _ => None);
 
 fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =