src/Pure/theory.ML
changeset 61261 ddb2da7cb2e4
parent 61256 9ce5de06cd3b
child 61262 7bd1eb4b056e
     1.1 --- a/src/Pure/theory.ML	Thu Sep 24 13:33:42 2015 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Sep 24 23:33:29 2015 +0200
     1.3 @@ -25,9 +25,9 @@
     1.4    val add_axiom: Proof.context -> binding * term -> theory -> theory
     1.5    val const_dep: theory -> string * typ -> Defs.entry
     1.6    val type_dep: string * typ list -> Defs.entry
     1.7 -  val add_deps: Proof.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
     1.8 +  val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
     1.9    val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
    1.10 -  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
    1.11 +  val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
    1.12    val specify_const: (binding * typ) * mixfix -> theory -> term * theory
    1.13    val check_overloading: Proof.context -> bool -> string * typ -> unit
    1.14  end
    1.15 @@ -75,12 +75,11 @@
    1.16  
    1.17    fun merge pp (thy1, thy2) =
    1.18      let
    1.19 -      val ctxt = Syntax.init_pretty pp;
    1.20        val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
    1.21        val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
    1.22  
    1.23        val axioms' = empty_axioms;
    1.24 -      val defs' = Defs.merge ctxt (defs1, defs2);
    1.25 +      val defs' = Defs.merge (Syntax.init_pretty pp, NONE) (defs1, defs2);
    1.26        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
    1.27        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
    1.28      in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
    1.29 @@ -216,7 +215,7 @@
    1.30  fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
    1.31  fun type_dep (c, args) = ((Defs.Type, c), args);
    1.32  
    1.33 -fun dependencies ctxt unchecked def description lhs rhs =
    1.34 +fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
    1.35    let
    1.36      val thy = Proof_Context.theory_of ctxt;
    1.37      val consts = Sign.consts_of thy;
    1.38 @@ -235,7 +234,7 @@
    1.39        else error ("Specification depends on extra type variables: " ^
    1.40          commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
    1.41          "\nThe error(s) above occurred in " ^ quote description);
    1.42 -  in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
    1.43 +  in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
    1.44  
    1.45  fun cert_entry thy ((Defs.Const, c), args) =
    1.46        Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
    1.47 @@ -243,14 +242,14 @@
    1.48    | cert_entry thy ((Defs.Type, c), args) =
    1.49        Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
    1.50  
    1.51 -fun add_deps ctxt a raw_lhs raw_rhs thy =
    1.52 +fun add_deps context a raw_lhs raw_rhs thy =
    1.53    let
    1.54      val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
    1.55      val description = if a = "" then lhs_name ^ " axiom" else a;
    1.56 -  in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
    1.57 +  in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
    1.58  
    1.59  fun add_deps_global a x y thy =
    1.60 -  add_deps (Syntax.init_pretty_global thy) a x y thy;
    1.61 +  add_deps (Syntax.init_pretty_global thy, NONE) a x y thy;
    1.62  
    1.63  fun specify_const decl thy =
    1.64    let val (t, thy') = Sign.declare_const_global decl thy;
    1.65 @@ -286,7 +285,7 @@
    1.66  
    1.67  local
    1.68  
    1.69 -fun check_def ctxt thy unchecked overloaded (b, tm) defs =
    1.70 +fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
    1.71    let
    1.72      val name = Sign.full_name thy b;
    1.73      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
    1.74 @@ -300,17 +299,17 @@
    1.75      val rhs_deps = rhs_consts @ rhs_types;
    1.76  
    1.77      val _ = check_overloading ctxt overloaded lhs_const;
    1.78 -  in defs |> dependencies ctxt unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
    1.79 +  in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
    1.80    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    1.81     [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
    1.82      Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
    1.83  
    1.84  in
    1.85  
    1.86 -fun add_def ctxt unchecked overloaded raw_axm thy =
    1.87 +fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
    1.88    let val axm = cert_axm ctxt raw_axm in
    1.89      thy
    1.90 -    |> map_defs (check_def ctxt thy unchecked overloaded axm)
    1.91 +    |> map_defs (check_def context thy unchecked overloaded axm)
    1.92      |> add_axiom ctxt axm
    1.93    end;
    1.94