src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 59484 a130ae7a9398
parent 59058 a78612c67ec0
child 59498 50b60f501b05
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 05 19:44:13 2015 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 05 19:44:14 2015 +0100
     1.3 @@ -166,6 +166,8 @@
     1.4  structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
     1.5  struct
     1.6  
     1.7 +val no_constr = [@{const_name STR}];
     1.8 +
     1.9  (* general functions *)
    1.10  
    1.11  fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
    1.12 @@ -504,7 +506,8 @@
    1.13        | _ => false)
    1.14    in check end
    1.15  
    1.16 -val is_constr = Code.is_constr o Proof_Context.theory_of
    1.17 +fun is_constr ctxt c =
    1.18 +  not (member (op =) no_constr c) andalso Code.is_constr (Proof_Context.theory_of ctxt) c;
    1.19  
    1.20  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
    1.21