src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 38795 848be46708dc
parent 38558 32ad17fe2b9c
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -405,7 +405,7 @@
     1.4  (* general syntactic functions *)
     1.5  
     1.6  (*Like dest_conj, but flattens conjunctions however nested*)
     1.7 -fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
     1.8 +fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
     1.9    | conjuncts_aux t conjs = t::conjs;
    1.10  
    1.11  fun conjuncts t = conjuncts_aux t [];