first working version of instance target

--- a/src/Pure/Isar/class.ML	Fri Nov 30 20:13:07 2007 +0100
+++ b/src/Pure/Isar/class.ML	Fri Nov 30 20:13:08 2007 +0100
@@ -210,7 +210,7 @@
   let
     val _ = if mx <> NoSyn then
       error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
-      else ()
+      else ();
     val SOME class = AxClass.class_of_param thy c;
     val SOME tyco = inst_tyco thy (c, ty);
     val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
@@ -841,32 +841,32 @@
 
 fun mk_instantiation (arities, params) =
   Instantiation { arities = arities, params = params };
-fun get_instantiation ctxt = case Instantiation.get ctxt
+fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
  of Instantiation data => data;
-fun map_instantiation f (Instantiation { arities, params }) =
-  mk_instantiation (f (arities, params));
+fun map_instantiation f = (LocalTheory.target o Instantiation.map)
+  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
 
-fun the_instantiation ctxt = case get_instantiation ctxt
+fun the_instantiation lthy = case get_instantiation lthy
  of { arities = [], ... } => error "No instantiation target"
   | data => data;
 
 val instantiation_params = #params o get_instantiation;
 
-fun instantiation_param ctxt v = instantiation_params ctxt
+fun instantiation_param lthy v = instantiation_params lthy
   |> find_first (fn (_, (v', _)) => v = v')
   |> Option.map (fst o fst);
 
-fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
+fun confirm_declaration c = (map_instantiation o apsnd)
   (filter_out (fn (_, (c', _)) => c' = c));
 
 
 (* syntax *)
 
-fun inst_term_check ts ctxt =
+fun inst_term_check ts lthy =
   let
-    val params = instantiation_params ctxt;
-    val tsig = ProofContext.tsig_of ctxt;
-    val thy = ProofContext.theory_of ctxt;
+    val params = instantiation_params lthy;
+    val tsig = ProofContext.tsig_of lthy;
+    val thy = ProofContext.theory_of lthy;
 
     fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
@@ -882,17 +882,17 @@
               | NONE => t)
           | NONE => t)
       | t => t) ts';
-  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
+  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
 
-fun inst_term_uncheck ts ctxt =
+fun inst_term_uncheck ts lthy =
   let
-    val params = instantiation_params ctxt;
+    val params = instantiation_params lthy;
     val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
        (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
          of SOME c => Const (c, ty)
           | NONE => t)
       | t => t) ts;
-  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
+  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
 
 
 (* target *)
@@ -946,8 +946,7 @@
 
 fun gen_instantiation_instance do_proof after_qed lthy =
   let
-    val ctxt = LocalTheory.target_of lthy;
-    val arities = (#arities o the_instantiation) ctxt;
+    val arities = (#arities o the_instantiation) lthy;
     val arities_proof = maps Logic.mk_arities arities;
     fun after_qed' results =
       LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)

--- a/src/Pure/Isar/instance.ML	Fri Nov 30 20:13:07 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Fri Nov 30 20:13:08 2007 +0100
@@ -61,9 +61,9 @@
     |> `(fn ctxt => map (mk_def ctxt) defs)
     |-> (fn defs => fold_map Specification.definition defs)
     |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
-    ||> LocalTheory.exit
-    ||> ProofContext.theory_of
-    ||> TheoryTarget.instantiation arities
+    ||> LocalTheory.reinit
+    (*||> ProofContext.theory_of
+    ||> TheoryTarget.instantiation arities*)
     |-> (fn defs => do_proof defs)
   else
     thy

--- a/src/Pure/Isar/theory_target.ML	Fri Nov 30 20:13:07 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Nov 30 20:13:08 2007 +0100
@@ -290,12 +290,7 @@
     val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
 
     (*axioms*)
-    val resubst_instparams = map_aterms (fn t as Free (v, T) =>
-      (case Class.instantiation_param lthy' v
-       of NONE => t
-        | SOME c => Const (c, T)) | t => t)
-    val hyps = map Thm.term_of (Assumption.assms_of lthy')
-      |> map resubst_instparams;
+    val hyps = map Thm.term_of (Assumption.assms_of lthy');
     fun axiom ((name, atts), props) thy = thy
       |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
       |-> (fn ths => pair ((name, atts), [(ths, [])]));