src/Pure/sign.ML
changeset 61262 7bd1eb4b056e
parent 59990 a81dc82ecba3
child 66245 da3b0e848182
     1.1 --- a/src/Pure/sign.ML	Thu Sep 24 23:33:29 2015 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Sep 25 19:13:47 2015 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4    val certify_sort: theory -> sort -> sort
     1.5    val certify_typ: theory -> typ -> typ
     1.6    val certify_typ_mode: Type.mode -> theory -> typ -> typ
     1.7 -  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
     1.8 +  val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int
     1.9    val certify_term: theory -> term -> term * typ * int
    1.10    val cert_term: theory -> term -> term
    1.11    val cert_prop: theory -> term -> term
    1.12 @@ -133,20 +133,20 @@
    1.13  
    1.14  fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
    1.15  
    1.16 -structure Data = Theory_Data_PP
    1.17 +structure Data = Theory_Data'
    1.18  (
    1.19    type T = sign;
    1.20    fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
    1.21  
    1.22    val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
    1.23  
    1.24 -  fun merge pp (sign1, sign2) =
    1.25 +  fun merge old_thys (sign1, sign2) =
    1.26      let
    1.27        val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
    1.28        val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.29  
    1.30        val syn = Syntax.merge_syntax (syn1, syn2);
    1.31 -      val tsig = Type.merge_tsig pp (tsig1, tsig2);
    1.32 +      val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
    1.33        val consts = Consts.merge (consts1, consts2);
    1.34      in make_sign (syn, tsig, consts) end;
    1.35  );
    1.36 @@ -257,7 +257,7 @@
    1.37  (* certify wrt. type signature *)
    1.38  
    1.39  val arity_number = Type.arity_number o tsig_of;
    1.40 -fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
    1.41 +fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy);
    1.42  
    1.43  val certify_class = Type.cert_class o tsig_of;
    1.44  val certify_sort = Type.cert_sort o tsig_of;
    1.45 @@ -269,14 +269,14 @@
    1.46  
    1.47  local
    1.48  
    1.49 -fun type_check pp tm =
    1.50 +fun type_check context tm =
    1.51    let
    1.52      fun err_appl bs t T u U =
    1.53        let
    1.54          val xs = map Free bs;           (*we do not rename here*)
    1.55          val t' = subst_bounds (xs, t);
    1.56          val u' = subst_bounds (xs, u);
    1.57 -        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
    1.58 +        val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U;
    1.59        in raise TYPE (msg, [T, U], [t', u']) end;
    1.60  
    1.61      fun typ_of (_, Const (_, T)) = T
    1.62 @@ -306,20 +306,19 @@
    1.63  
    1.64  in
    1.65  
    1.66 -fun certify' prop pp do_expand consts thy tm =
    1.67 +fun certify' prop context do_expand consts thy tm =
    1.68    let
    1.69      val _ = check_vars tm;
    1.70      val tm' = Term.map_types (certify_typ thy) tm;
    1.71 -    val T = type_check pp tm';
    1.72 +    val T = type_check context tm';
    1.73      val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
    1.74 -    val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
    1.75 +    val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm';
    1.76    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
    1.77  
    1.78 -fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
    1.79 -fun cert_term_abbrev thy =
    1.80 -  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
    1.81 +fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;
    1.82 +fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy;
    1.83  val cert_term = #1 oo certify_term;
    1.84 -fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
    1.85 +fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy;
    1.86  
    1.87  end;
    1.88  
    1.89 @@ -474,10 +473,10 @@
    1.90    |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
    1.91  
    1.92  fun primitive_classrel arg thy =
    1.93 -  thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
    1.94 +  thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg);
    1.95  
    1.96  fun primitive_arity arg thy =
    1.97 -  thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
    1.98 +  thy |> map_tsig (Type.add_arity (Context.Theory thy) arg);
    1.99  
   1.100  
   1.101  (* add translation functions *)