src/Pure/Isar/attrib.ML
changeset 39557 fe5722fce758
parent 39507 839873937ddd
child 40291 012ed4426fda
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4  fun gen_thm pick = Scan.depend (fn context =>
     1.5    let
     1.6      val thy = Context.theory_of context;
     1.7 -    val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
     1.8 +    val get = Context.cases (Global_Theory.get_fact context) ProofContext.get_fact context;
     1.9      val get_fact = get o Facts.Fact;
    1.10      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    1.11    in