src/HOLCF/fixrec_package.ML

       PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
     val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
     
     fun mk_cterm t = cterm_of thy' (infer thy' t);
     val ctuple_unfold_ct = mk_cterm (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
-    val ctuple_unfold_thm = prove_goalw_cterm [] ctuple_unfold_ct
+    val ctuple_unfold_thm = OldGoals.prove_goalw_cterm [] ctuple_unfold_ct
           (fn _ => [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
                     simp_tac (simpset_of thy') 1]);
     val ctuple_induct_thm =
           (space_implode "_" names ^ "_induct", ctuple_fixdef_thm RS def_fix_ind);
     

 (* proves a block of pattern matching equations as theorems, using unfold *)
 fun make_simps thy (unfold_thm, eqns) =
   let
     fun tacsf prems =
       [rtac (unfold_thm RS ssubst_lhs) 1, simp_tac (simpset_of thy addsimps prems) 1];
-    fun prove_term t = prove_goalw_cterm [] (cterm_of thy t) tacsf;
+    fun prove_term t = OldGoals.prove_goalw_cterm [] (cterm_of thy t) tacsf;
     fun prove_eqn ((name, eqn_t), atts) = ((name, prove_term eqn_t), atts);
   in
     map prove_eqn eqns
   end;
 

     val T = fastype_of t;
     val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
     val cname = case chead_of t of Const(c,_) => c | _ =>
               fixrec_err "function is not declared as constant in theory";
     val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
-    val simp = prove_goalw_cterm [] (cterm_of thy eq)
+    val simp = OldGoals.prove_goalw_cterm [] (cterm_of thy eq)
           (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   in simp end;
 
 fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
   let