src/HOL/Tools/inductive_package.ML
changeset 30089 f631fb528277
parent 29868 787349bb53e9
child 30190 479806475f3c
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Feb 25 11:07:10 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Feb 25 11:20:34 2009 +0100
     1.3 @@ -738,7 +738,7 @@
     1.4      val _ = message (quiet_mode andalso not verbose)
     1.5        ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
     1.6  
     1.7 -    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
     1.8 +    val cnames = map (LocalTheory.full_name ctxt o #1) cnames_syn;  (* FIXME *)
     1.9      val ((intr_names, intr_atts), intr_ts) =
    1.10        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
    1.11