# HG changeset patch
# User haftmann
# Date 1213104665 -7200
# Node ID ac87245d8cab921deb79011539b873f93a89ff5a
# Parent  661a74bafeb797ff7ac580e75431d5ffe4ede798
dropped instance with attached definitions

diff -r 661a74bafeb7 -r ac87245d8cab src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Tue Jun 10 15:31:04 2008 +0200
+++ b/src/Pure/Isar/instance.ML	Tue Jun 10 15:31:05 2008 +0200
@@ -2,25 +2,17 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-A primitive instance command, based on instantiation target.
+Wrapper for instantiation command.
 *)
 
 signature INSTANCE =
 sig
   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
 end;
 
 structure Instance : INSTANCE =
 struct
 
-fun read_single_arity thy (raw_tyco, raw_sorts, raw_sort) =
-  let
-    val (tyco, sorts, sort) = Sign.read_arity thy (raw_tyco, raw_sorts, raw_sort);
-    val vs = Name.names Name.context Name.aT sorts;
-  in (tyco, vs, sort) end;
-
 fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   let
     val all_arities = map (fn raw_tyco => Sign.read_arity thy
@@ -33,32 +25,4 @@
 fun instantiation_cmd raw_arities thy =
   TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
 
-fun instance_cmd raw_arities defs thy =
-  let
-    val (tyco, vs, sort) = read_single_arity thy raw_arities;
-    fun mk_def ctxt ((name, raw_attr), raw_t) =
-      let
-        val attr = map (Attrib.intern_src thy) raw_attr;
-        val t = Syntax.parse_prop ctxt raw_t;
-      in (NONE, ((name, attr), t)) end;
-    fun define def ctxt =
-      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 definitions; use instantiation instead." else ();
-  in if null defs
-  then
-    thy
-    |> Class.instance_arity I (tyco, map snd vs, sort)
-  else
-    thy
-    |> TheoryTarget.instantiation ([tyco], vs, sort)
-    |> `(fn ctxt => map (mk_def ctxt) defs)
-    |-> (fn defs => fold_map Specification.definition defs)
-    |> snd
-    |> LocalTheory.restore
-    |> Class.instantiation_instance Class.conclude_instantiation
-  end;
-
 end;
diff -r 661a74bafeb7 -r ac87245d8cab src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 10 15:31:04 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 10 15:31:05 2008 +0200
@@ -443,8 +443,7 @@
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
-      >> (fn (arity, defs) => Instance.instance_cmd arity defs))
+    P.arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof)
   || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));