1.1 --- a/src/Pure/codegen.ML	Tue May 12 21:39:19 2009 +0200
     1.2 +++ b/src/Pure/codegen.ML	Wed May 13 19:21:32 2009 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    val mk_type: bool -> typ -> Pretty.T
     1.5    val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
     1.6    val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
     1.7 -  val test_fn: (int -> (string * term) list option) ref
     1.8 +  val test_fn: (int -> term list option) ref
     1.9    val test_term: Proof.context -> term -> int -> term list option
    1.10    val eval_result: (unit -> term) ref
    1.11    val eval_term: theory -> term -> term
    1.12 @@ -871,39 +871,35 @@
    1.13                [mk_gen gr module true xs a T, mk_type true T]) Ts) @
    1.14           (if member (op =) xs s then [str a] else []))));
    1.15  
    1.16 -val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
    1.17 +val test_fn : (int -> term list option) ref = ref (fn _ => NONE);
    1.18  
    1.19  fun test_term ctxt t =
    1.20    let
    1.21      val thy = ProofContext.theory_of ctxt;
    1.22      val (code, gr) = setmp mode ["term_of", "test"]
    1.23        (generate_code_i thy [] "Generated") [("testf", t)];
    1.24 -    val frees = Name.names Name.context "a" ((map snd o fst o strip_abs) t);
    1.25 -    val frees' = frees ~~
    1.26 -      map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
    1.27 +    val Ts = map snd (fst (strip_abs t));
    1.28 +    val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
    1.29      val s = "structure TestTerm =\nstruct\n\n" ^
    1.30        cat_lines (map snd code) ^
    1.31        "\nopen Generated;\n\n" ^ string_of
    1.32          (Pretty.block [str "val () = Codegen.test_fn :=",
    1.33            Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
    1.34 -          mk_let (map (fn ((s, T), s') =>
    1.35 -              (mk_tuple [str s', str (s' ^ "_t")],
    1.36 +          mk_let (map (fn (s, T) =>
    1.37 +              (mk_tuple [str s, str (s ^ "_t")],
    1.38                 Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
    1.39 -                 str "(i + 1)"])) frees')
    1.40 +                 str "i"])) args)
    1.41              (Pretty.block [str "if ",
    1.42 -              mk_app false (str "testf") (map (str o snd) frees'),
    1.43 +              mk_app false (str "testf") (map (str o fst) args),
    1.44                Pretty.brk 1, str "then NONE",
    1.45                Pretty.brk 1, str "else ",
    1.46                Pretty.block [str "SOME ", Pretty.block (str "[" ::
    1.47 -                flat (separate [str ",", Pretty.brk 1]
    1.48 -                  (map (fn ((s, T), s') => [Pretty.block
    1.49 -                    [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
    1.50 -                     str (s' ^ "_t ())")]]) frees')) @
    1.51 +                Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
    1.52                    [str "]"])]]),
    1.53            str ");"]) ^
    1.54        "\n\nend;\n";
    1.55      val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
    1.56 -  in ! test_fn #> (Option.map o map) snd end;
    1.57 +  in ! test_fn end;
    1.58  
    1.59  
    1.60