src/Tools/Code/code_target.ML
changeset 42359 6ca5407863ed
parent 41940 a3b68a7a0e15
child 42361 23f352990944
     1.1 --- a/src/Tools/Code/code_target.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -307,13 +307,16 @@
     1.4  
     1.5  fun project_program thy abortable names_hidden names1 program2 =
     1.6    let
     1.7 +    val ctxt = ProofContext.init_global thy;
     1.8      val names2 = subtract (op =) names_hidden names1;
     1.9      val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
    1.10      val names4 = Graph.all_succs program3 names2;
    1.11      val empty_funs = filter_out (member (op =) abortable)
    1.12        (Code_Thingol.empty_funs program3);
    1.13 -    val _ = if null empty_funs then () else error ("No code equations for "
    1.14 -      ^ commas (map (Sign.extern_const thy) empty_funs));
    1.15 +    val _ =
    1.16 +      if null empty_funs then ()
    1.17 +      else error ("No code equations for " ^
    1.18 +        commas (map (ProofContext.extern_const ctxt) empty_funs));
    1.19      val program4 = Graph.subgraph (member (op =) names4) program3;
    1.20    in (names4, program4) end;
    1.21