src/Tools/Code/code_haskell.ML
changeset 37437 4202e11ae7dc
parent 37384 5aba26803073
child 37439 c72a43a7d2c5
equal deleted inserted replaced
37433:a2a89563bfcb 37437:4202e11ae7dc
   113             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
   113             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
   114             (map print_select clauses)
   114             (map print_select clauses)
   115           end
   115           end
   116       | print_case tyvars some_thm vars fxy ((_, []), _) =
   116       | print_case tyvars some_thm vars fxy ((_, []), _) =
   117           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   117           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   118     fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
   118     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
   119           let
   119           let
   120             val tyvars = intro_vars (map fst vs) reserved;
   120             val tyvars = intro_vars (map fst vs) reserved;
   121             fun print_err n =
   121             fun print_err n =
   122               semicolon (
   122               semicolon (
   123                 (str o deresolve_base) name
   123                 (str o deresolve_base) name