src/HOL/HOL.thy
changeset 42422 6a2837ddde4b
parent 42420 8a09dfeb2cec
parent 42411 ff997038e8eb
child 42426 7ec150fcf3dc
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 20 10:14:24 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 20 11:21:12 2011 +0200
     1.3 @@ -1746,20 +1746,21 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 -fun eq_codegen thy defs dep thyname b t gr =
     1.8 +fun eq_codegen thy mode defs dep thyname b t gr =
     1.9      (case strip_comb t of
    1.10         (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
    1.11       | (Const (@{const_name HOL.eq}, _), [t, u]) =>
    1.12            let
    1.13 -            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    1.14 -            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    1.15 -            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
    1.16 +            val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr;
    1.17 +            val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr';
    1.18 +            val (_, gr''') =
    1.19 +              Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr'';
    1.20            in
    1.21              SOME (Codegen.parens
    1.22                (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    1.23            end
    1.24       | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
    1.25 -         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.26 +         thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.27       | _ => NONE);
    1.28  
    1.29  in