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 **)

     2.1 --- a/src/Tools/Code/code_namespace.ML	Thu Apr 19 08:45:13 2012 +0200
     2.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Apr 19 10:16:51 2012 +0200
     2.3 @@ -78,8 +78,8 @@
     2.4        end;
     2.5      fun add_dependency name name' =
     2.6        let
     2.7 -        val (module_name, base) = dest_name name;
     2.8 -        val (module_name', base') = dest_name name';
     2.9 +        val (module_name, _) = dest_name name;
    2.10 +        val (module_name', _) = dest_name name';
    2.11        in if module_name = module_name'
    2.12          then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
    2.13          else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
    2.14 @@ -177,8 +177,8 @@
    2.15        end;
    2.16      fun add_dependency name name' =
    2.17        let
    2.18 -        val (name_fragments, base) = dest_name name;
    2.19 -        val (name_fragments', base') = dest_name name';
    2.20 +        val (name_fragments, _) = dest_name name;
    2.21 +        val (name_fragments', _) = dest_name name';
    2.22          val (name_fragments_common, (diff, diff')) =
    2.23            chop_prefix (op =) (name_fragments, name_fragments');
    2.24          val is_module = not (null diff andalso null diff');

     3.1 --- a/src/Tools/Code/code_printer.ML	Thu Apr 19 08:45:13 2012 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Thu Apr 19 10:16:51 2012 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4            |> pair false;
     3.5          fun filter (XML.Elem (name_attrs, xs)) =
     3.6                fold (if is_selected name_attrs then add_content_with_space else filter) xs
     3.7 -          | filter (XML.Text s) = I;
     3.8 +          | filter (XML.Text _) = I;
     3.9        in snd (fold filter tree (true, Buffer.empty)) end;
    3.10  
    3.11  fun format presentation_names width =

     4.1 --- a/src/Tools/Code/code_simp.ML	Thu Apr 19 08:45:13 2012 +0200
     4.2 +++ b/src/Tools/Code/code_simp.ML	Thu Apr 19 10:16:51 2012 +0200
     4.3 @@ -53,7 +53,7 @@
     4.4  (* evaluation with dynamic code context *)
     4.5  
     4.6  fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
     4.7 -  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program);
     4.8 +  (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
     4.9  
    4.10  fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;
    4.11  

     5.1 --- a/src/Tools/Code/code_target.ML	Thu Apr 19 08:45:13 2012 +0200
     5.2 +++ b/src/Tools/Code/code_target.ML	Thu Apr 19 10:16:51 2012 +0200
     5.3 @@ -270,7 +270,7 @@
     5.4  
     5.5  fun activate_target thy target =
     5.6    let
     5.7 -    val ((targets, abortable), default_width) = Targets.get thy;
     5.8 +    val ((_, abortable), default_width) = Targets.get thy;
     5.9      val (modify, data) = collapse_hierarchy thy target;
    5.10    in (default_width, abortable, data, modify) end;
    5.11  
    5.12 @@ -630,7 +630,7 @@
    5.13  
    5.14  local
    5.15  
    5.16 -fun zip_list (x::xs) f g =
    5.17 +fun zip_list (x :: xs) f g =
    5.18    f
    5.19    :|-- (fn y =>
    5.20      fold_map (fn x => g |-- f >> pair x) xs

     6.1 --- a/src/Tools/Code/code_thingol.ML	Thu Apr 19 08:45:13 2012 +0200
     6.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Apr 19 10:16:51 2012 +0200
     6.3 @@ -436,8 +436,7 @@
     6.4  type program = stmt Graph.T;
     6.5  
     6.6  fun empty_funs program =
     6.7 -  Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
     6.8 -               | _ => I) program [];
     6.9 +  Graph.fold (fn (_, (Fun (c, ((_, []), _)), _)) => cons c | _ => I) program [];
    6.10  
    6.11  fun map_terms_bottom_up f (t as IConst _) = f t
    6.12    | map_terms_bottom_up f (t as IVar _) = f t
    6.13 @@ -533,21 +532,24 @@
    6.14      val (name, naming') = case lookup naming thing
    6.15       of SOME name => (name, naming)
    6.16        | NONE => declare thing naming;
    6.17 -  in case try (Graph.get_node program) name
    6.18 -   of SOME stmt => program
    6.19 -        |> add_dep name
    6.20 -        |> pair naming'
    6.21 -        |> pair dep
    6.22 -        |> pair name
    6.23 -    | NONE => program
    6.24 -        |> Graph.default_node (name, NoStmt)
    6.25 -        |> add_dep name
    6.26 -        |> pair naming'
    6.27 -        |> curry generate (SOME name)
    6.28 -        ||> snd
    6.29 -        |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
    6.30 -        |> pair dep
    6.31 -        |> pair name
    6.32 +  in
    6.33 +    if can (Graph.get_node program) name
    6.34 +    then
    6.35 +      program
    6.36 +      |> add_dep name
    6.37 +      |> pair naming'
    6.38 +      |> pair dep
    6.39 +      |> pair name
    6.40 +    else
    6.41 +      program
    6.42 +      |> Graph.default_node (name, NoStmt)
    6.43 +      |> add_dep name
    6.44 +      |> pair naming'
    6.45 +      |> curry generate (SOME name)
    6.46 +      ||> snd
    6.47 +      |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
    6.48 +      |> pair dep
    6.49 +      |> pair name
    6.50    end;
    6.51  
    6.52  exception PERMISSIVE of unit;
    6.53 @@ -588,7 +590,7 @@
    6.54  fun tag_term (proj_sort, _) eqngr =
    6.55    let
    6.56      val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr;
    6.57 -    fun tag (Const (c', T')) (Const (c, T)) =
    6.58 +    fun tag (Const (_, T')) (Const (c, T)) =
    6.59          Const (c,
    6.60            mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
    6.61        | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u
    6.62 @@ -965,7 +967,7 @@
    6.63  
    6.64  fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
    6.65    let
    6.66 -    val (((_, program'), (((vs', ty'), t'), deps)), _) =
    6.67 +    val (((_, _), (((vs', ty'), t'), deps)), _) =
    6.68        ensure_value thy algebra eqngr t (NONE, (naming, program));
    6.69    in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
    6.70  
    6.71 @@ -982,7 +984,7 @@
    6.72    let
    6.73      fun generate_consts thy algebra eqngr =
    6.74        fold_map (ensure_const thy algebra eqngr false);
    6.75 -    val (consts', (naming, program)) =
    6.76 +    val (_, (_, program)) =
    6.77        invoke_generation true thy (algebra, eqngr) generate_consts consts;
    6.78    in evaluator' program end;
    6.79  

     7.1 --- a/src/Tools/misc_legacy.ML	Thu Apr 19 08:45:13 2012 +0200
     7.2 +++ b/src/Tools/misc_legacy.ML	Thu Apr 19 10:16:51 2012 +0200
     7.3 @@ -260,7 +260,7 @@
     7.4       val thy = Thm.theory_of_thm fth
     7.5   in
     7.6     case Thm.fold_terms Term.add_vars fth [] of
     7.7 -       [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
     7.8 +       [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
     7.9       | vars =>
    7.10           let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
    7.11               val alist = map newName vars

     8.1 --- a/src/Tools/quickcheck.ML	Thu Apr 19 08:45:13 2012 +0200
     8.2 +++ b/src/Tools/quickcheck.ML	Thu Apr 19 10:16:51 2012 +0200
     8.3 @@ -137,14 +137,6 @@
     8.4    | set_response _ _ NONE result = result
     8.5  
     8.6  
     8.7 -fun set_counterexample counterexample (Result r) =
     8.8 -  Result {counterexample = counterexample,  evaluation_terms = #evaluation_terms r,
     8.9 -    timings = #timings r, reports = #reports r}
    8.10 -
    8.11 -fun set_evaluation_terms evaluation_terms (Result r) =
    8.12 -  Result {counterexample = #counterexample r,  evaluation_terms = evaluation_terms,
    8.13 -    timings = #timings r, reports = #reports r}
    8.14 -
    8.15  fun cons_timing timing (Result r) =
    8.16    Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
    8.17      timings = cons timing (#timings r), reports = #reports r}
    8.18 @@ -288,8 +280,6 @@
    8.19  val mk_batch_validator =
    8.20    gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
    8.21    
    8.22 -fun lookup_tester ctxt = AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)
    8.23 -
    8.24  (* testing propositions *)
    8.25  
    8.26  type compile_generator =
    8.27 @@ -413,27 +403,11 @@
    8.28       @ [pretty_stat "positive conclusion tests" positive_concl_tests])
    8.29    end
    8.30  
    8.31 -fun pretty_reports ctxt (SOME reports) =
    8.32 -  Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" ::
    8.33 -    maps (fn (size, report) =>
    8.34 -      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
    8.35 -      (rev reports))
    8.36 -  | pretty_reports ctxt NONE = Pretty.str ""
    8.37 -
    8.38  fun pretty_timings timings =
    8.39    Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" ::
    8.40      maps (fn (label, time) =>
    8.41        Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
    8.42  
    8.43 -fun pretty_counterex_and_reports ctxt auto [] =
    8.44 -    Pretty.chunks [Pretty.strs (tool_name auto ::
    8.45 -        space_explode " " "is used in a locale where no interpretation is provided."),
    8.46 -      Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
    8.47 -  | pretty_counterex_and_reports ctxt auto (result :: _) =
    8.48 -    Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
    8.49 -      (* map (pretty_reports ctxt) (reports_of result) :: *)
    8.50 -      (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
    8.51 -
    8.52  (* Isar commands *)
    8.53  
    8.54  fun read_nat s = case (Library.read_int o Symbol.explode) s