synchronize_syntax: declare operations within the local scope of fixes/consts
authorwenzelm
Tue Nov 06 22:50:36 2007 +0100 (2007-11-06)
changeset 25318c8352b38d47d
parent 25317 8b38b394fa8e
child 25319 074d41176558
synchronize_syntax: declare operations within the local scope of fixes/consts
(still inactive -- breaks rogue type-inference of rule_tac/where/of);
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Nov 06 22:50:35 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Nov 06 22:50:36 2007 +0100
     1.3 @@ -634,7 +634,11 @@
     1.4      val constraints = (map o apsnd) (fst o snd) operations;
     1.5  
     1.6      (* check phase *)
     1.7 -    val typargs = Consts.typargs (ProofContext.consts_of ctxt);
     1.8 +    val consts = ProofContext.consts_of ctxt;
     1.9 +    fun declare_const (c, _) =
    1.10 +      let val b = Sign.base_name c
    1.11 +      in if Consts.intern consts b = c then Variable.declare_const b else I end;
    1.12 +    val typargs = Consts.typargs consts;
    1.13      fun check_const (c, ty) (t, (_, typidx)) = ((nth (typargs (c, ty)) typidx), t);
    1.14      fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
    1.15        |> Option.map (check_const c_ty);
    1.16 @@ -647,6 +651,7 @@
    1.17        |> (map o pairself o map_types) basify;
    1.18    in
    1.19      ctxt
    1.20 +(*    |> fold declare_const operations  FIXME *)
    1.21      |> fold (ProofContext.add_const_constraint o local_constraint) operations
    1.22      |> ClassSyntax.put (SOME {
    1.23          constraints = constraints,
    1.24 @@ -871,7 +876,7 @@
    1.25    in
    1.26      thy'
    1.27      |> Sign.declare_const pos (c, ty'', mx) |> snd
    1.28 -    |> Thm.add_def false (c, def_eq)
    1.29 +    |> Thm.add_def false (c, def_eq)    (* FIXME PureThy.add_defs_i *)
    1.30      |>> Thm.symmetric
    1.31      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
    1.32            #> register_operation class (c', ((dict, dict'), SOME (Thm.varifyT def))))