src/HOL/Tools/inductive.ML
changeset 56249 0fda98dd2c93
parent 56245 84fc7dfa3cd4
child 56334 6b3739fee456
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Mar 22 15:58:27 2014 +0100
     1.3 @@ -1000,7 +1000,9 @@
     1.4      cnames_syn pnames spec monos lthy =
     1.5    let
     1.6      val thy = Proof_Context.theory_of lthy;
     1.7 -    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
     1.8 +    val _ =
     1.9 +      Theory.requires thy (Context.theory_name @{theory})
    1.10 +        (coind_prefix coind ^ "inductive definitions");
    1.11  
    1.12  
    1.13      (* abbrevs *)