src/Pure/Isar/class.ML
changeset 25514 4b508bb31a6c
parent 25502 9200b36280c0
child 25518 00d5cc16e891
     1.1 --- a/src/Pure/Isar/class.ML	Fri Nov 30 20:13:07 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Nov 30 20:13:08 2007 +0100
     1.3 @@ -210,7 +210,7 @@
     1.4    let
     1.5      val _ = if mx <> NoSyn then
     1.6        error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
     1.7 -      else ()
     1.8 +      else ();
     1.9      val SOME class = AxClass.class_of_param thy c;
    1.10      val SOME tyco = inst_tyco thy (c, ty);
    1.11      val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
    1.12 @@ -841,32 +841,32 @@
    1.13  
    1.14  fun mk_instantiation (arities, params) =
    1.15    Instantiation { arities = arities, params = params };
    1.16 -fun get_instantiation ctxt = case Instantiation.get ctxt
    1.17 +fun get_instantiation lthy = case Instantiation.get (LocalTheory.target_of lthy)
    1.18   of Instantiation data => data;
    1.19 -fun map_instantiation f (Instantiation { arities, params }) =
    1.20 -  mk_instantiation (f (arities, params));
    1.21 +fun map_instantiation f = (LocalTheory.target o Instantiation.map)
    1.22 +  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
    1.23  
    1.24 -fun the_instantiation ctxt = case get_instantiation ctxt
    1.25 +fun the_instantiation lthy = case get_instantiation lthy
    1.26   of { arities = [], ... } => error "No instantiation target"
    1.27    | data => data;
    1.28  
    1.29  val instantiation_params = #params o get_instantiation;
    1.30  
    1.31 -fun instantiation_param ctxt v = instantiation_params ctxt
    1.32 +fun instantiation_param lthy v = instantiation_params lthy
    1.33    |> find_first (fn (_, (v', _)) => v = v')
    1.34    |> Option.map (fst o fst);
    1.35  
    1.36 -fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
    1.37 +fun confirm_declaration c = (map_instantiation o apsnd)
    1.38    (filter_out (fn (_, (c', _)) => c' = c));
    1.39  
    1.40  
    1.41  (* syntax *)
    1.42  
    1.43 -fun inst_term_check ts ctxt =
    1.44 +fun inst_term_check ts lthy =
    1.45    let
    1.46 -    val params = instantiation_params ctxt;
    1.47 -    val tsig = ProofContext.tsig_of ctxt;
    1.48 -    val thy = ProofContext.theory_of ctxt;
    1.49 +    val params = instantiation_params lthy;
    1.50 +    val tsig = ProofContext.tsig_of lthy;
    1.51 +    val thy = ProofContext.theory_of lthy;
    1.52  
    1.53      fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
    1.54           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.55 @@ -882,17 +882,17 @@
    1.56                | NONE => t)
    1.57            | NONE => t)
    1.58        | t => t) ts';
    1.59 -  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
    1.60 +  in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end;
    1.61  
    1.62 -fun inst_term_uncheck ts ctxt =
    1.63 +fun inst_term_uncheck ts lthy =
    1.64    let
    1.65 -    val params = instantiation_params ctxt;
    1.66 +    val params = instantiation_params lthy;
    1.67      val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
    1.68         (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
    1.69           of SOME c => Const (c, ty)
    1.70            | NONE => t)
    1.71        | t => t) ts;
    1.72 -  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
    1.73 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
    1.74  
    1.75  
    1.76  (* target *)
    1.77 @@ -946,8 +946,7 @@
    1.78  
    1.79  fun gen_instantiation_instance do_proof after_qed lthy =
    1.80    let
    1.81 -    val ctxt = LocalTheory.target_of lthy;
    1.82 -    val arities = (#arities o the_instantiation) ctxt;
    1.83 +    val arities = (#arities o the_instantiation) lthy;
    1.84      val arities_proof = maps Logic.mk_arities arities;
    1.85      fun after_qed' results =
    1.86        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)