src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 54742 7a86358a3c0b
parent 53887 ee91bd2a506a
child 55399 5c8e91f884af
child 55437 3fd63b92ea3b
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -1017,8 +1017,9 @@
     1.4  
     1.5  fun peephole_optimisation thy intro =
     1.6    let
     1.7 +    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     1.8      val process =
     1.9 -      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
    1.10 +      rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
    1.11      fun process_False intro_t =
    1.12        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
    1.13      fun process_True intro_t =