src/HOL/Predicate_Compile.thy
changeset 69593 3dda49e08b9d
parent 67613 ce654b0e6d69
child 69605 a96320074298
     1.1 --- a/src/HOL/Predicate_Compile.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -80,14 +80,14 @@
     1.4    val ii = Fun (Input, Fun (Input, Bool))
     1.5  in
     1.6    Core_Data.PredData.map (Graph.new_node 
     1.7 -    (@{const_name contains}, 
     1.8 +    (\<^const_name>\<open>contains\<close>, 
     1.9       Core_Data.PredData {
    1.10         pos = Position.thread_data (),
    1.11         intros = [(NONE, @{thm containsI})], 
    1.12         elim = SOME @{thm containsE}, 
    1.13         preprocessed = true,
    1.14         function_names = [(Predicate_Compile_Aux.Pred, 
    1.15 -         [(io, @{const_name pred_of_set}), (ii, @{const_name contains_pred})])], 
    1.16 +         [(io, \<^const_name>\<open>pred_of_set\<close>), (ii, \<^const_name>\<open>contains_pred\<close>)])], 
    1.17         predfun_data = [
    1.18           (io, Core_Data.PredfunData {
    1.19              elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI},