cleanup

--- a/src/HOL/Tools/function_package/auto_term.ML	Thu Mar 22 11:17:32 2007 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Thu Mar 22 13:36:55 2007 +0100
@@ -23,8 +23,8 @@
       val rule = FundefCommon.get_termination_rule ctxt |> the
                   |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
 
-      val prem = #1 (Logic.dest_implies (Thm.prop_of rule))
-      val Rvar = cert (Var (the_single (Term.add_vars prem [])))
+      val _ $ premise $ _ = Thm.prop_of rule
+      val Rvar = cert (Var (the_single (Term.add_vars premise [])))
     in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end
 
 

--- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Mar 22 11:17:32 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Mar 22 13:36:55 2007 +0100
@@ -479,9 +479,9 @@
           Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
                                 Abs ("y", ranT, G $ Bound 1 $ Bound 0))
               |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
-          
+
       val ((f, (_, f_defthm)), lthy) =
-        LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
+        LocalTheory.def Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
     in
       ((f, f_defthm), lthy)
     end
@@ -897,7 +897,7 @@
           PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
       val (_, lthy) = 
-          LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R) lthy
+          LocalTheory.abbrev Syntax.default_mode ((dom_name defname, NoSyn), mk_acc domT R) lthy
 
       val newthy = ProofContext.theory_of lthy
       val clauses = map (transfer_clause_ctx newthy) clauses