src/HOL/String.thy
changeset 42411 ff997038e8eb
parent 42163 392fd6c4669c
child 42440 5e7a7343ab11
     1.1 --- a/src/HOL/String.thy	Tue Apr 19 22:32:49 2011 +0200
     1.2 +++ b/src/HOL/String.thy	Tue Apr 19 23:57:28 2011 +0200
     1.3 @@ -227,10 +227,10 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 -fun char_codegen thy defs dep thyname b t gr =
     1.8 +fun char_codegen thy mode defs dep thyname b t gr =
     1.9    let
    1.10      val i = HOLogic.dest_char t;
    1.11 -    val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
    1.12 +    val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
    1.13        (fastype_of t) gr;
    1.14    in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
    1.15    end handle TERM _ => NONE;