dropped Instance.instantiate

--- a/src/HOL/Library/Eval.thy	Fri Dec 07 10:59:03 2007 +0100
+++ b/src/HOL/Library/Eval.thy	Fri Dec 07 15:07:54 2007 +0100
@@ -40,8 +40,12 @@
       val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
     in
       thy
-      |> Instance.instantiate ([tyco], sorts, @{sort typ_of})
-           (define_typ_of ty) ((K o K) (Class.intro_classes_tac []))
+      |> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of})
+      |> define_typ_of ty
+      |> snd
+      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+      |> LocalTheory.exit
+      |> ProofContext.theory_of
     end;
 in TypedefPackage.interpretation interpretator end
 *}
@@ -158,8 +162,12 @@
   fun interpretator tycos thy = case prep thy tycos
    of SOME (sorts, defs) =>
       thy
-      |> Instance.instantiate (tycos, sorts, @{sort term_of})
-           (primrec defs) ((K o K) (Class.intro_classes_tac []))
+      |> TheoryTarget.instantiation (tycos, sorts, @{sort term_of})
+      |> primrec defs
+      |> snd
+      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+      |> LocalTheory.exit
+      |> ProofContext.theory_of
     | NONE => thy;
   in DatatypePackage.interpretation interpretator end
 *}
@@ -185,13 +193,20 @@
 by pat_completeness auto
 termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
 
-instance int :: term_of
-  "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
+instantiation int :: term_of
+begin
+
+definition
+  "term_of k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
+
+instance ..
+
+end
 
 
 text {* Adaption for @{typ message_string}s *}
 
-lemmas [code func del] = term_of_messagestring.simps
+lemmas [code func del] = term_of_message_string.simps
 
 
 subsection {* Evaluation infrastructure *}

--- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 07 10:59:03 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 07 15:07:54 2007 +0100
@@ -435,8 +435,10 @@
       map (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq] o snd) vs;
   in
     thy
-    |> Instance.instantiate (dtcos, sorts_eq, [HOLogic.class_eq]) (pair ())
-         ((K o K) (Class.intro_classes_tac []))
+    |> TheoryTarget.instantiation (dtcos, sorts_eq, [HOLogic.class_eq])
+    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+    |> LocalTheory.exit
+    |> ProofContext.theory_of
     |> fold add_eq_thms dtcos
   end;
 

--- a/src/HOL/Tools/function_package/size.ML	Fri Dec 07 10:59:03 2007 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Fri Dec 07 15:07:54 2007 +0100
@@ -33,9 +33,13 @@
 val size_name_base = NameSpace.base size_name;
 val size_suffix = "_" ^ size_name_base;
 
-fun instance_size_class tyco thy = thy |> Instance.instantiate
-  ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
-    (pair ()) ((K o K) (Class.intro_classes_tac []));
+fun instance_size_class tyco thy =
+  thy
+  |> TheoryTarget.instantiation
+       ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
+  |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+  |> LocalTheory.exit
+  |> ProofContext.theory_of;
 
 fun plus (t1, t2) = Const ("HOL.plus_class.plus",
   HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;

--- a/src/HOL/Tools/typecopy_package.ML	Fri Dec 07 10:59:03 2007 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Fri Dec 07 15:07:54 2007 +0100
@@ -131,8 +131,10 @@
     thy
     |> Code.add_datatype [(constr, ty)]
     |> Code.add_func proj_def
-    |> Instance.instantiate ([tyco], sorts_eq, [HOLogic.class_eq]) (pair ())
-         ((K o K) (Class.intro_classes_tac []))
+    |> TheoryTarget.instantiation ([tyco], sorts_eq, [HOLogic.class_eq])
+    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+    |> LocalTheory.exit
+    |> ProofContext.theory_of
     |> Code.add_func (CodeUnit.constrain_thm [HOLogic.class_eq] inject)
   end;
 

--- a/src/Pure/Isar/instance.ML	Fri Dec 07 10:59:03 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Fri Dec 07 15:07:54 2007 +0100
@@ -7,9 +7,6 @@
 
 signature INSTANCE =
 sig
-  val instantiate: string list * sort list * sort -> (local_theory -> 'a * local_theory)
-    -> (Proof.context -> 'a -> tactic) -> theory -> theory
-
   val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
   val instance_cmd: xstring * sort * xstring -> ((bstring * Attrib.src list) * xstring) list
     -> theory -> Proof.state
@@ -29,13 +26,6 @@
 fun instantiation_cmd raw_arities thy =
   TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
 
-fun instantiate arities f tac =
-  TheoryTarget.instantiation arities
-  #> f
-  #-> (fn result => Class.prove_instantiation_instance (fn ctxt => tac ctxt result))
-  #> LocalTheory.exit
-  #> ProofContext.theory_of;
-
 fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
   let
     val (tyco, sorts, sort) = prep_arity thy raw_arities;
@@ -56,6 +46,8 @@
       let
         val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
       in Specification.definition def' ctxt end;
+    val _ = if not (null defs) then Output.legacy_feature
+      "Instance command with attached attached definitions; use instantiation instead." else ();
   in if not (null defs) orelse forall (Class.is_class thy) sort
   then
     thy