src/Tools/Code/code_thingol.ML

   type program = stmt Graph.T
   val empty_funs: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_cons: program -> string -> bool
+  val is_case: stmt -> bool
   val contr_classparam_typs: program -> string -> itype option list
   val labelled_name: theory -> program -> string -> string
   val group_stmts: theory -> program
     -> ((string * stmt) list * (string * stmt) list
       * ((string * stmt) list * (string * stmt) list)) list

 
 fun is_cons program name = case Graph.get_node program name
  of Datatypecons _ => true
   | _ => false;
 
+fun is_case (Fun (_, (_, SOME _))) = true
+  | is_case _ = false;
+
 fun contr_classparam_typs program name = case Graph.get_node program name
  of Classparam (_, class) => let
         val Class (_, (_, (_, params))) = Graph.get_node program class;
         val SOME ty = AList.lookup (op =) params name;
         val (tys, res_ty) = unfold_fun ty;

   | Classparam (c, _) => quote (Code.string_of_const thy c)
   | Classinst ((class, (tyco, _)), _) => let
         val Class (class, _) = Graph.get_node program class
         val Datatype (tyco, _) = Graph.get_node program tyco
       in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
+
+fun linear_stmts program =
+  rev (Graph.strong_conn program)
+  |> map (AList.make (Graph.get_node program));
 
 fun group_stmts thy program =
   let
     fun is_fun (_, Fun _) = true | is_fun _ = false;
     fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;

       else if forall (is_fun orf is_classinst) stmts
       then ([], [], List.partition is_fun stmts)
       else error ("Illegal mutual dependencies: " ^
         (commas o map (labelled_name thy program o fst)) stmts)
   in
-    rev (Graph.strong_conn program)
-    |> map (AList.make (Graph.get_node program))
+    linear_stmts program
     |> map group
   end;
 
 
 (** translation kernel **)

       ensure_class thy algbr eqngr permissive class
       #>> (fn class => Classparam (c, class));
     fun stmt_fun cert =
       let
         val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
+        val some_case_cong = Code.get_case_cong thy c;
       in
         fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
         ##>> translate_typ thy algbr eqngr permissive ty
-        ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns
-          #>> map_filter I)
-        #>> (fn info => Fun (c, (info, NONE)))
+        ##>> translate_eqns thy algbr eqngr permissive eqns
+        #>> (fn info => Fun (c, (info, some_case_cong)))
       end;
     val stmt_const = case Code.get_type_of_constr_or_abstr thy c
      of SOME (tyco, _) => stmt_datatypecons tyco
       | NONE => (case AxClass.class_of_param thy c
          of SOME class => stmt_classparam class

             #>> (fn (t, ts) => t `$$ ts)
 and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
   fold_map (translate_term thy algbr eqngr permissive some_thm) args
   ##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
   #>> rpair (some_thm, proper)
-and translate_equation thy algbr eqngr permissive eqn prgrm =
-  prgrm |> translate_eqn thy algbr eqngr permissive eqn |>> SOME
-    handle PERMISSIVE () => (NONE, prgrm)
+and translate_eqns thy algbr eqngr permissive eqns prgrm =
+  prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns
+    handle PERMISSIVE () => ([], prgrm)
 and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
   let
     val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
         andalso Code.is_abstr thy c
         then translation_error thy permissive some_thm