src/HOL/Tools/TFL/post.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30686 47a32dd1b86e
     1.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4   *---------------------------------------------------------------------------*)
     1.5  fun define_i strict thy cs ss congs wfs fid R eqs =
     1.6    let val {functional,pats} = Prim.mk_functional thy eqs
     1.7 -      val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional
     1.8 +      val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
     1.9        val {induct, rules, tcs} = 
    1.10            simplify_defn strict thy cs ss congs wfs fid pats def
    1.11        val rules' = 
    1.12 @@ -248,7 +248,7 @@
    1.13  
    1.14  fun defer_i thy congs fid eqs =
    1.15   let val {rules,R,theory,full_pats_TCs,SV,...} =
    1.16 -             Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs
    1.17 +             Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs
    1.18       val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
    1.19       val dummy = writeln "Proving induction theorem ...";
    1.20       val induction = Prim.mk_induction theory