src/HOL/Mutabelle/Mutabelle.thy
changeset 39557 fe5722fce758
parent 38864 4abe644fcea5
child 42361 23f352990944
     1.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -75,12 +75,12 @@
     1.4  fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
     1.5     Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
     1.6     is_executable thy th)
     1.7 - (PureThy.all_thms_of thy);
     1.8 + (Global_Theory.all_thms_of thy);
     1.9  
    1.10  fun find_thm thy = find_first (fn (_, th) => not (Thm.is_internal th) andalso
    1.11     Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
    1.12     is_executable thy th)
    1.13 - (PureThy.all_thms_of thy);
    1.14 + (Global_Theory.all_thms_of thy);
    1.15  *}
    1.16  
    1.17  ML {*