1.1 --- a/src/Tools/Code/code_ml.ML	Thu Apr 19 08:45:13 2012 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Apr 19 10:16:51 2012 +0200
     1.3 @@ -42,12 +42,6 @@
     1.4  fun stmt_name_of_binding (ML_Function (name, _)) = name
     1.5    | stmt_name_of_binding (ML_Instance (name, _)) = name;
     1.6  
     1.7 -fun stmt_names_of (ML_Exc (name, _)) = [name]
     1.8 -  | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
     1.9 -  | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
    1.10 -  | stmt_names_of (ML_Datas ds) = map fst ds
    1.11 -  | stmt_names_of (ML_Class (name, _)) = [name];
    1.12 -
    1.13  fun print_product _ [] = NONE
    1.14    | print_product print [x] = SOME (print x)
    1.15    | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    1.16 @@ -59,7 +53,7 @@
    1.17  
    1.18  (** SML serializer **)
    1.19  
    1.20 -fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
    1.21 +fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    1.22    let
    1.23      fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.24        | print_tyco_expr fxy (tyco, [ty]) =
    1.25 @@ -363,7 +357,7 @@
    1.26  
    1.27  (** OCaml serializer **)
    1.28  
    1.29 -fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
    1.30 +fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    1.31    let
    1.32      fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    1.33        | print_tyco_expr fxy (tyco, [ty]) =
    1.34 @@ -372,7 +366,7 @@
    1.35            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    1.36      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.37           of NONE => print_tyco_expr fxy (tyco, tys)
    1.38 -          | SOME (i, print) => print print_typ fxy tys)
    1.39 +          | SOME (_, print) => print print_typ fxy tys)
    1.40        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    1.41      fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    1.42      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    1.43 @@ -435,7 +429,7 @@
    1.44      and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    1.45            let
    1.46              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.47 -            fun print_let ((pat, ty), t) vars =
    1.48 +            fun print_let ((pat, _), t) vars =
    1.49                vars
    1.50                |> print_bind is_pseudo_fun some_thm NOBR pat
    1.51                |>> (fn p => concat
    1.52 @@ -764,7 +758,7 @@
    1.53      fun modify_class stmts = single (SOME
    1.54        (ML_Class (the_single (map_filter
    1.55          (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
    1.56 -    fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) =
    1.57 +    fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
    1.58            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
    1.59        | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
    1.60            modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
    1.61 @@ -790,7 +784,7 @@
    1.62        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
    1.63    end;
    1.64  
    1.65 -fun serialize_ml target print_ml_module print_ml_stmt with_signatures
    1.66 +fun serialize_ml print_ml_module print_ml_stmt with_signatures
    1.67      { labelled_name, reserved_syms, includes, module_alias,
    1.68        class_syntax, tyco_syntax, const_syntax } program =
    1.69    let
    1.70 @@ -801,12 +795,12 @@
    1.71  
    1.72      (* print statements *)
    1.73      fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
    1.74 -      labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
    1.75 +      tyco_syntax const_syntax (make_vars reserved_syms)
    1.76        (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
    1.77        |> apfst SOME;
    1.78  
    1.79      (* print modules *)
    1.80 -    fun print_module prefix_fragments base _ xs =
    1.81 +    fun print_module _ base _ xs =
    1.82        let
    1.83          val (raw_decls, body) = split_list xs;
    1.84          val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
    1.85 @@ -825,13 +819,11 @@
    1.86  
    1.87  val serializer_sml : Code_Target.serializer =
    1.88    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    1.89 -  >> (fn with_signatures => serialize_ml target_SML
    1.90 -      print_sml_module print_sml_stmt with_signatures));
    1.91 +  >> (fn with_signatures => serialize_ml print_sml_module print_sml_stmt with_signatures));
    1.92  
    1.93  val serializer_ocaml : Code_Target.serializer =
    1.94    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    1.95 -  >> (fn with_signatures => serialize_ml target_OCaml
    1.96 -      print_ocaml_module print_ocaml_stmt with_signatures));
    1.97 +  >> (fn with_signatures => serialize_ml print_ocaml_module print_ocaml_stmt with_signatures));
    1.98  
    1.99  
   1.100  (** Isar setup **)