src/HOL/Mutabelle/Mutabelle.thy
changeset 42361 23f352990944
parent 39557 fe5722fce758
child 46711 f745bcc4a1e5
     1.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -61,16 +61,16 @@
     1.4  
     1.5  (*
     1.6  ML {*
     1.7 -Quickcheck.test_term (ProofContext.init_global @{theory})
     1.8 +Quickcheck.test_term (Proof_Context.init_global @{theory})
     1.9   false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
    1.10  *}
    1.11  
    1.12  ML {*
    1.13  fun is_executable thy th = can (Quickcheck.test_term
    1.14 - (ProofContext.init_global thy) false (SOME "SML") 1 1) (prop_of th);
    1.15 + (Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th);
    1.16  
    1.17  fun is_executable_term thy t = can (Quickcheck.test_term
    1.18 - (ProofContext.init_global thy) false (SOME "SML") 1 1) t;
    1.19 + (Proof_Context.init_global thy) false (SOME "SML") 1 1) t;
    1.20  
    1.21  fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
    1.22     Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso