src/Pure/Isar/class.ML

 
 fun overloaded_const (c, ty, mx) thy =
   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";
     val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
     val ty' = Type.strip_sorts ty;

   fun init _ = Instantiation { arities = [], params = [] };
 );
 
 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 the_instantiation ctxt = case get_instantiation ctxt
+fun map_instantiation f = (LocalTheory.target o Instantiation.map)
+  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
+
+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 =
-  let
-    val params = instantiation_params ctxt;
-    val tsig = ProofContext.tsig_of ctxt;
-    val thy = ProofContext.theory_of ctxt;
+fun inst_term_check ts lthy =
+  let
+    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)
              of SOME (_, ty') => perhaps (try (Type.typ_match tsig (ty, ty')))
               | NONE => I)

          of SOME tyco => (case AList.lookup (op =) params (c, tyco)
              of SOME v_ty => Free v_ty
               | NONE => t)
           | NONE => t)
       | t => t) ts';
-  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
-
-fun inst_term_uncheck ts ctxt =
-  let
-    val params = instantiation_params ctxt;
+  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
+
+fun inst_term_uncheck ts lthy =
+  let
+    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 *)
 
 val sanatize_name = (*FIXME*)

         #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
   end;
 
 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)
       #> after_qed;
   in