src/Pure/goals.ML
changeset 16458 4c6fd0c01d28
parent 16335 37aabcf75ee1
child 16486 1a12cdb6ee6b
     1.1 --- a/src/Pure/goals.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/goals.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Pure/goals.ML
     1.5 +(*  Title:      Pure/goals.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson and Florian Kammueller, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Old-style locales and goal stack package.  The goal stack initially
    1.12 @@ -19,71 +19,71 @@
    1.13    val thms: xstring -> thm list
    1.14    type proof
    1.15    val reset_goals       : unit -> unit
    1.16 -  val atomic_goal	: theory -> string -> thm list
    1.17 -  val atomic_goalw	: theory -> thm list -> string -> thm list
    1.18 -  val Goal		: string -> thm list
    1.19 -  val Goalw		: thm list -> string -> thm list
    1.20 -  val ba		: int -> unit
    1.21 -  val back		: unit -> unit
    1.22 -  val bd		: thm -> int -> unit
    1.23 -  val bds		: thm list -> int -> unit
    1.24 -  val be		: thm -> int -> unit
    1.25 -  val bes		: thm list -> int -> unit
    1.26 -  val br		: thm -> int -> unit
    1.27 -  val brs		: thm list -> int -> unit
    1.28 -  val bw		: thm -> unit
    1.29 -  val bws		: thm list -> unit
    1.30 -  val by		: tactic -> unit
    1.31 -  val byev		: tactic list -> unit
    1.32 -  val chop		: unit -> unit
    1.33 -  val choplev		: int -> unit
    1.34 +  val atomic_goal       : theory -> string -> thm list
    1.35 +  val atomic_goalw      : theory -> thm list -> string -> thm list
    1.36 +  val Goal              : string -> thm list
    1.37 +  val Goalw             : thm list -> string -> thm list
    1.38 +  val ba                : int -> unit
    1.39 +  val back              : unit -> unit
    1.40 +  val bd                : thm -> int -> unit
    1.41 +  val bds               : thm list -> int -> unit
    1.42 +  val be                : thm -> int -> unit
    1.43 +  val bes               : thm list -> int -> unit
    1.44 +  val br                : thm -> int -> unit
    1.45 +  val brs               : thm list -> int -> unit
    1.46 +  val bw                : thm -> unit
    1.47 +  val bws               : thm list -> unit
    1.48 +  val by                : tactic -> unit
    1.49 +  val byev              : tactic list -> unit
    1.50 +  val chop              : unit -> unit
    1.51 +  val choplev           : int -> unit
    1.52    val export_thy        : theory -> thm -> thm
    1.53    val export            : thm -> thm
    1.54 -  val Export		: thm -> thm
    1.55 -  val fa		: unit -> unit
    1.56 -  val fd		: thm -> unit
    1.57 -  val fds		: thm list -> unit
    1.58 -  val fe		: thm -> unit
    1.59 -  val fes		: thm list -> unit
    1.60 -  val filter_goal	: (term*term->bool) -> thm list -> int -> thm list
    1.61 -  val fr		: thm -> unit
    1.62 -  val frs		: thm list -> unit
    1.63 -  val getgoal		: int -> term
    1.64 -  val gethyps		: int -> thm list
    1.65 -  val goal		: theory -> string -> thm list
    1.66 -  val goalw		: theory -> thm list -> string -> thm list
    1.67 -  val goalw_cterm	: thm list -> cterm -> thm list
    1.68 -  val pop_proof		: unit -> thm list
    1.69 -  val pr		: unit -> unit
    1.70 +  val Export            : thm -> thm
    1.71 +  val fa                : unit -> unit
    1.72 +  val fd                : thm -> unit
    1.73 +  val fds               : thm list -> unit
    1.74 +  val fe                : thm -> unit
    1.75 +  val fes               : thm list -> unit
    1.76 +  val filter_goal       : (term*term->bool) -> thm list -> int -> thm list
    1.77 +  val fr                : thm -> unit
    1.78 +  val frs               : thm list -> unit
    1.79 +  val getgoal           : int -> term
    1.80 +  val gethyps           : int -> thm list
    1.81 +  val goal              : theory -> string -> thm list
    1.82 +  val goalw             : theory -> thm list -> string -> thm list
    1.83 +  val goalw_cterm       : thm list -> cterm -> thm list
    1.84 +  val pop_proof         : unit -> thm list
    1.85 +  val pr                : unit -> unit
    1.86    val disable_pr        : unit -> unit
    1.87    val enable_pr         : unit -> unit
    1.88 -  val prlev		: int -> unit
    1.89 -  val prlim		: int -> unit
    1.90 -  val premises		: unit -> thm list
    1.91 -  val prin		: term -> unit
    1.92 -  val printyp		: typ -> unit
    1.93 -  val pprint_term	: term -> pprint_args -> unit
    1.94 -  val pprint_typ	: typ -> pprint_args -> unit
    1.95 -  val print_exn		: exn -> 'a
    1.96 -  val print_sign_exn	: Sign.sg -> exn -> 'a
    1.97 -  val prove_goal	: theory -> string -> (thm list -> tactic list) -> thm
    1.98 +  val prlev             : int -> unit
    1.99 +  val prlim             : int -> unit
   1.100 +  val premises          : unit -> thm list
   1.101 +  val prin              : term -> unit
   1.102 +  val printyp           : typ -> unit
   1.103 +  val pprint_term       : term -> pprint_args -> unit
   1.104 +  val pprint_typ        : typ -> pprint_args -> unit
   1.105 +  val print_exn         : exn -> 'a
   1.106 +  val print_sign_exn    : theory -> exn -> 'a
   1.107 +  val prove_goal        : theory -> string -> (thm list -> tactic list) -> thm
   1.108    val prove_goalw      : theory->thm list->string->(thm list->tactic list)->thm
   1.109 -  val prove_goalw_cterm	: thm list->cterm->(thm list->tactic list)->thm
   1.110 -  val prove_goalw_cterm_nocheck	: thm list->cterm->(thm list->tactic list)->thm
   1.111 +  val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm
   1.112 +  val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm
   1.113    val quick_and_dirty_prove_goalw_cterm: theory -> thm list -> cterm
   1.114      -> (thm list -> tactic list) -> thm
   1.115    val simple_prove_goal_cterm : cterm->(thm list->tactic list)->thm
   1.116 -  val push_proof	: unit -> unit
   1.117 -  val read		: string -> term
   1.118 -  val ren		: string -> int -> unit
   1.119 -  val restore_proof	: proof -> thm list
   1.120 -  val result		: unit -> thm  
   1.121 +  val push_proof        : unit -> unit
   1.122 +  val read              : string -> term
   1.123 +  val ren               : string -> int -> unit
   1.124 +  val restore_proof     : proof -> thm list
   1.125 +  val result            : unit -> thm
   1.126    val result_error_fn   : (thm -> string -> thm) ref
   1.127 -  val rotate_proof	: unit -> thm list
   1.128 -  val uresult		: unit -> thm  
   1.129 -  val save_proof	: unit -> proof
   1.130 -  val topthm		: unit -> thm
   1.131 -  val undo		: unit -> unit
   1.132 +  val rotate_proof      : unit -> thm list
   1.133 +  val uresult           : unit -> thm
   1.134 +  val save_proof        : unit -> proof
   1.135 +  val topthm            : unit -> thm
   1.136 +  val undo              : unit -> unit
   1.137    val bind_thm          : string * thm -> unit
   1.138    val bind_thms         : string * thm list -> unit
   1.139    val qed               : string -> unit
   1.140 @@ -112,7 +112,7 @@
   1.141    val open_locale: xstring -> theory -> theory
   1.142    val close_locale: xstring -> theory -> theory
   1.143    val print_scope: theory -> unit
   1.144 -  val read_cterm: Sign.sg -> string * typ -> cterm
   1.145 +  val read_cterm: theory -> string * typ -> cterm
   1.146  end;
   1.147  
   1.148  structure Goals: GOALS =
   1.149 @@ -125,11 +125,11 @@
   1.150  
   1.151      locale Locale_name =
   1.152        fixes   (*variables that are fixed in the locale's scope*)
   1.153 -	v :: T
   1.154 +        v :: T
   1.155        assumes (*meta-hypothesis that hold in the locale*)
   1.156 -	Asm_name "meta-formula"  
   1.157 +        Asm_name "meta-formula"
   1.158        defines (*local definitions of fixed variables in terms of others*)
   1.159 -	v_def "v x == ...x..."
   1.160 +        v_def "v x == ...x..."
   1.161  *)
   1.162  
   1.163  (** type locale **)
   1.164 @@ -144,13 +144,13 @@
   1.165    defaults: (string * sort) list * (string * typ) list * string list};
   1.166  
   1.167  fun make_locale ancestor consts nosyn rules defs thms defaults =
   1.168 -  {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules, 
   1.169 +  {ancestor = ancestor, consts = consts, nosyn = nosyn, rules = rules,
   1.170     defs = defs, thms = thms, defaults = defaults}: locale;
   1.171  
   1.172 -fun pretty_locale sg (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
   1.173 +fun pretty_locale thy (name, {ancestor, consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
   1.174    let
   1.175 -    val prt_typ = Pretty.quote o Sign.pretty_typ sg;
   1.176 -    val prt_term = Pretty.quote o Sign.pretty_term sg;
   1.177 +    val prt_typ = Pretty.quote o Sign.pretty_typ thy;
   1.178 +    val prt_term = Pretty.quote o Sign.pretty_term thy;
   1.179  
   1.180      fun pretty_const (c, T) = Pretty.block
   1.181        [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
   1.182 @@ -182,48 +182,43 @@
   1.183  fun make_locale_data space locales scope =
   1.184    {space = space, locales = locales, scope = scope}: locale_data;
   1.185  
   1.186 -structure LocalesArgs =
   1.187 -struct
   1.188 +structure LocalesData = TheoryDataFun
   1.189 +(struct
   1.190    val name = "Pure/old-locales";
   1.191    type T = locale_data;
   1.192  
   1.193    val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
   1.194    fun copy {space, locales, scope = ref locs} = make_locale_data space locales (ref locs);
   1.195 -  fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
   1.196 -  fun merge ({space = space1, locales = locales1, scope = _},
   1.197 +  fun extend {space, locales, scope = _} = make_locale_data space locales (ref []);
   1.198 +  fun merge _ ({space = space1, locales = locales1, scope = _},
   1.199      {space = space2, locales = locales2, scope = _}) =
   1.200        make_locale_data (NameSpace.merge (space1, space2))
   1.201          (Symtab.merge (K true) (locales1, locales2))
   1.202          (ref []);
   1.203  
   1.204 -  fun print sg {space, locales, scope} =
   1.205 +  fun print thy {space, locales, scope} =
   1.206      let
   1.207        val locs = NameSpace.extern_table (space, locales);
   1.208        val scope_names = rev (map (NameSpace.extern space o fst) (! scope));
   1.209      in
   1.210 -      [Display.pretty_name_space ("locale name space", space),
   1.211 -        Pretty.big_list "locales:" (map (pretty_locale sg) locs),
   1.212 +      [Pretty.big_list "locales:" (map (pretty_locale thy) locs),
   1.213          Pretty.strs ("current scope:" :: scope_names)]
   1.214        |> Pretty.chunks |> Pretty.writeln
   1.215      end;
   1.216 -end;
   1.217 +end);
   1.218  
   1.219 -
   1.220 -structure LocalesData = TheoryDataFun(LocalesArgs);
   1.221  val _ = Context.add_setup [LocalesData.init];
   1.222  val print_locales = LocalesData.print;
   1.223  
   1.224  
   1.225  (* access locales *)
   1.226  
   1.227 -fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
   1.228 -
   1.229 -val get_locale = get_locale_sg o Theory.sign_of;
   1.230 +fun get_locale thy name = Symtab.lookup (#locales (LocalesData.get thy), name);
   1.231  
   1.232  fun put_locale (name, locale) thy =
   1.233    let
   1.234      val {space, locales, scope} = LocalesData.get thy;
   1.235 -    val space' = Sign.declare_name (Theory.sign_of thy) name space;
   1.236 +    val space' = Sign.declare_name thy name space;
   1.237      val locales' = Symtab.update ((name, locale), locales);
   1.238    in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
   1.239  
   1.240 @@ -236,11 +231,9 @@
   1.241  
   1.242  (* access scope *)
   1.243  
   1.244 -fun get_scope_sg sg =
   1.245 -  if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then []
   1.246 -  else ! (#scope (LocalesData.get_sg sg));
   1.247 -
   1.248 -val get_scope = get_scope_sg o Theory.sign_of;
   1.249 +fun get_scope thy =
   1.250 +  if eq_thy (thy, ProtoPure.thy) then []
   1.251 +  else ! (#scope (LocalesData.get thy));
   1.252  
   1.253  fun change_scope f thy =
   1.254    let val {scope, ...} = LocalesData.get thy
   1.255 @@ -264,26 +257,26 @@
   1.256        fun opn lc th = (change_scope (cons lc) th; th)
   1.257    in case anc of
   1.258           NONE => opn loc thy
   1.259 -       | SOME(loc') => 
   1.260 -           if loc' mem (map fst cur_sc) 
   1.261 +       | SOME(loc') =>
   1.262 +           if loc' mem (map fst cur_sc)
   1.263             then opn loc thy
   1.264 -           else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^ 
   1.265 -			  quote xname);
   1.266 +           else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^
   1.267 +                          quote xname);
   1.268                   opn loc (open_locale (Sign.base_name loc') thy))
   1.269    end;
   1.270  
   1.271  fun pop_locale [] = error "Currently no open locales"
   1.272    | pop_locale (_ :: locs) = locs;
   1.273  
   1.274 -fun close_locale name thy = 
   1.275 +fun close_locale name thy =
   1.276     let val lname = (case get_scope thy of (ln,_)::_ => ln
   1.277                                          | _ => error "No locales are open!")
   1.278 -       val ok = (name = Sign.base_name lname) handle _ => false
   1.279 +       val ok = name = Sign.base_name lname
   1.280     in if ok then (change_scope pop_locale thy; thy)
   1.281        else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
   1.282     end;
   1.283  
   1.284 -fun print_scope thy = 
   1.285 +fun print_scope thy =
   1.286  Pretty.writeln (Pretty.strs ("current scope:" :: rev(map (Sign.base_name o fst) (get_scope thy))));
   1.287  
   1.288  (*implicit context versions*)
   1.289 @@ -295,11 +288,10 @@
   1.290  (** functions for goals.ML **)
   1.291  
   1.292  (* in_locale: check if hyps (: term list) of a proof are contained in the
   1.293 -   (current) scope. This function is needed in prepare_proof. It needs to
   1.294 -   refer to the signature, because theory is not available in prepare_proof. *)
   1.295 +   (current) scope. This function is needed in prepare_proof. *)
   1.296  
   1.297 -fun in_locale hyps sg =
   1.298 -    let val cur_sc = get_scope_sg sg;
   1.299 +fun in_locale hyps thy =
   1.300 +    let val cur_sc = get_scope thy;
   1.301          val rule_lists = map (#rules o snd) cur_sc;
   1.302          val def_lists = map (#defs o snd) cur_sc;
   1.303          val rules = map snd (foldr (op union) [] rule_lists);
   1.304 @@ -311,12 +303,10 @@
   1.305  
   1.306  
   1.307  (* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
   1.308 -fun is_open_loc_sg sign =
   1.309 -    let val cur_sc = get_scope_sg sign
   1.310 +fun is_open_loc thy =
   1.311 +    let val cur_sc = get_scope thy
   1.312      in not(null(cur_sc)) end;
   1.313  
   1.314 -val is_open_loc = is_open_loc_sg o Theory.sign_of;
   1.315 -
   1.316  
   1.317  (* get theorems *)
   1.318  
   1.319 @@ -336,7 +326,7 @@
   1.320  
   1.321  (* get the defaults of a locale, for extension *)
   1.322  
   1.323 -fun get_defaults thy name = 
   1.324 +fun get_defaults thy name =
   1.325    let val (lname, loc) = the_locale thy name;
   1.326    in #defaults(loc)
   1.327    end;
   1.328 @@ -346,15 +336,15 @@
   1.329  
   1.330  (* prepare types *)
   1.331  
   1.332 -fun read_typ sg (envT, s) =
   1.333 +fun read_typ thy (envT, s) =
   1.334    let
   1.335      fun def_sort (x, ~1) = assoc (envT, x)
   1.336        | def_sort _ = NONE;
   1.337 -    val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
   1.338 +    val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg;
   1.339    in (Term.add_typ_tfrees (T, envT), T) end;
   1.340  
   1.341 -fun cert_typ sg (envT, raw_T) =
   1.342 -  let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
   1.343 +fun cert_typ thy (envT, raw_T) =
   1.344 +  let val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg
   1.345    in (Term.add_typ_tfrees (T, envT), T) end;
   1.346  
   1.347  
   1.348 @@ -365,20 +355,20 @@
   1.349  fun enter_term t (envS, envT, used) =
   1.350    (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
   1.351  
   1.352 -fun read_axm sg ((envS, envT, used), (name, s)) =
   1.353 +fun read_axm thy ((envS, envT, used), (name, s)) =
   1.354    let
   1.355      fun def_sort (x, ~1) = assoc (envS, x)
   1.356        | def_sort _ = NONE;
   1.357      fun def_type (x, ~1) = assoc (envT, x)
   1.358        | def_type _ = NONE;
   1.359 -    val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
   1.360 +    val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s);
   1.361    in
   1.362      (enter_term t (envS, envT, used), t)
   1.363    end;
   1.364  
   1.365  
   1.366 -fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
   1.367 -  let val (_, t) = Theory.cert_axm sg (name, raw_t)
   1.368 +fun cert_axm thy ((envS, envT, used), (name, raw_t)) =
   1.369 +  let val (_, t) = Theory.cert_axm thy (name, raw_t)
   1.370    in (enter_term t (envS, envT, used), t) end;
   1.371  
   1.372  
   1.373 @@ -386,8 +376,8 @@
   1.374     that already exist for subterms. If no locale is open, this function is equal to
   1.375     Thm.read_cterm  *)
   1.376  
   1.377 -fun read_cterm sign =
   1.378 -    let val cur_sc = get_scope_sg sign;
   1.379 +fun read_cterm thy =
   1.380 +    let val cur_sc = get_scope thy;
   1.381          val defaults = map (#defaults o snd) cur_sc;
   1.382          val envS = List.concat (map #1 defaults);
   1.383          val envT = List.concat (map #2 defaults);
   1.384 @@ -396,15 +386,15 @@
   1.385            | def_sort _ = NONE;
   1.386          fun def_type (x, ~1) = assoc (envT, x)
   1.387            | def_type _ = NONE;
   1.388 -    in (if (is_open_loc_sg sign)
   1.389 -        then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
   1.390 -        else Thm.read_cterm sign)
   1.391 +    in (if (is_open_loc thy)
   1.392 +        then (#1 o read_def_cterm (thy, def_type, def_sort) used true)
   1.393 +        else Thm.read_cterm thy)
   1.394      end;
   1.395  
   1.396  (* basic functions needed for definitions and display *)
   1.397  (* collect all locale constants of a scope, i.e. a list of locales *)
   1.398 -fun collect_consts sg =
   1.399 -    let val cur_sc = get_scope_sg sg;
   1.400 +fun collect_consts thy =
   1.401 +    let val cur_sc = get_scope thy;
   1.402          val locale_list = map snd cur_sc;
   1.403          val const_list = List.concat (map #consts locale_list)
   1.404      in map fst const_list end;
   1.405 @@ -447,7 +437,7 @@
   1.406  
   1.407  (* assume a definition, i.e assume the cterm of a definiton term and then eliminate
   1.408     the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
   1.409 -fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
   1.410 +fun prep_hyps clist thy = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of thy);
   1.411  
   1.412  
   1.413  (* concrete syntax *)
   1.414 @@ -460,21 +450,20 @@
   1.415  (* add_locale *)
   1.416  
   1.417  fun gen_add_locale prep_typ prep_term bname bancestor raw_consts raw_rules raw_defs thy =
   1.418 -  let val sign = Theory.sign_of thy;
   1.419 +  let
   1.420 +    val name = Sign.full_name thy bname;
   1.421  
   1.422 -    val name = Sign.full_name sign bname;
   1.423 -
   1.424 -    val (envSb, old_loc_consts, _) = 
   1.425 +    val (envSb, old_loc_consts, _) =
   1.426                      case bancestor of
   1.427                         SOME(loc) => (get_defaults thy loc)
   1.428                       | NONE      => ([],[],[]);
   1.429  
   1.430 -    val old_nosyn = case bancestor of 
   1.431 +    val old_nosyn = case bancestor of
   1.432                         SOME(loc) => #nosyn(#2(the_locale thy loc))
   1.433                       | NONE      => [];
   1.434  
   1.435      (* Get the full name of the ancestor *)
   1.436 -    val ancestor = case bancestor of 
   1.437 +    val ancestor = case bancestor of
   1.438                         SOME(loc) => SOME(#1(the_locale thy loc))
   1.439                       | NONE      => NONE;
   1.440  
   1.441 @@ -485,7 +474,7 @@
   1.442          val c = Syntax.const_name raw_c raw_mx;
   1.443          val c_syn = mark_syn c;
   1.444          val mx = Syntax.fix_mixfix raw_c raw_mx;
   1.445 -        val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
   1.446 +        val (envS', T) = prep_typ thy (envS, raw_T) handle ERROR =>
   1.447            error ("The error(s) above occured in locale constant " ^ quote c);
   1.448          val trfun = if mx = Syntax.NoSyn then NONE else SOME (c_syn, mk_loc_tr c);
   1.449        in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
   1.450 @@ -505,38 +494,36 @@
   1.451        |> Theory.add_modesyntax_i Syntax.default_mode loc_syn
   1.452        |> Theory.add_trfuns ([], loc_trfuns, [], []);
   1.453  
   1.454 -    val syntax_sign = Theory.sign_of syntax_thy;
   1.455 -
   1.456  
   1.457      (* prepare rules and defs *)
   1.458  
   1.459      fun prep_axiom (env, (a, raw_t)) =
   1.460        let
   1.461 -        val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
   1.462 +        val (env', t) = prep_term syntax_thy (env, (a, raw_t)) handle ERROR =>
   1.463            error ("The error(s) above occured in locale rule / definition " ^ quote a);
   1.464        in (env', (a, t)) end;
   1.465  
   1.466      val ((envS1, envT1, used1), loc_rules) =
   1.467        foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
   1.468 -    val (defaults, loc_defs) = 
   1.469 -	foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
   1.470 +    val (defaults, loc_defs) =
   1.471 +        foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
   1.472  
   1.473 -    val old_loc_consts = collect_consts syntax_sign;
   1.474 +    val old_loc_consts = collect_consts syntax_thy;
   1.475      val new_loc_consts = (map #1 loc_consts);
   1.476      val all_loc_consts = old_loc_consts @ new_loc_consts;
   1.477  
   1.478 -    val (defaults, loc_defs_terms) = 
   1.479 -	foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
   1.480 -    val loc_defs_thms = 
   1.481 -	map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
   1.482 -    val (defaults, loc_thms_terms) = 
   1.483 -	foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
   1.484 -    val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign))
   1.485 -		       (loc_thms_terms)
   1.486 +    val (defaults, loc_defs_terms) =
   1.487 +        foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
   1.488 +    val loc_defs_thms =
   1.489 +        map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy)) loc_defs_terms;
   1.490 +    val (defaults, loc_thms_terms) =
   1.491 +        foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
   1.492 +    val loc_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_thy))
   1.493 +                       (loc_thms_terms)
   1.494                     @ loc_defs_thms;
   1.495  
   1.496  
   1.497 -    (* error messages *) 
   1.498 +    (* error messages *)
   1.499  
   1.500      fun locale_error msg = error (msg ^ "\nFor locale " ^ quote name);
   1.501  
   1.502 @@ -544,31 +531,31 @@
   1.503        if is_none (get_locale thy name) then []
   1.504        else ["Duplicate definition of locale " ^ quote name];
   1.505  
   1.506 -    (* check if definientes are locale constants 
   1.507 +    (* check if definientes are locale constants
   1.508         (in the same locale, so no redefining!) *)
   1.509      val err_def_head =
   1.510 -      let fun peal_appl t = 
   1.511 -            case t of 
   1.512 +      let fun peal_appl t =
   1.513 +            case t of
   1.514                   t1 $ t2 => peal_appl t1
   1.515                 | Free(t) => t
   1.516                 | _ => locale_error ("Bad form of LHS in locale definition");
   1.517 -	  fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
   1.518 -	    | lhs _ = locale_error ("Definitions must use the == relation");
   1.519 +          fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
   1.520 +            | lhs _ = locale_error ("Definitions must use the == relation");
   1.521            val defs = map lhs loc_defs;
   1.522            val check = defs subset loc_consts
   1.523 -      in if check then [] 
   1.524 +      in if check then []
   1.525           else ["defined item not declared fixed in locale " ^ quote name]
   1.526 -      end; 
   1.527 +      end;
   1.528  
   1.529      (* check that variables on rhs of definitions are either fixed or on lhs *)
   1.530 -    val err_var_rhs = 
   1.531 -      let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
   1.532 -		let val varl1 = difflist d1 all_loc_consts;
   1.533 -		    val varl2 = difflist d2 all_loc_consts
   1.534 -		in t andalso (varl2 subset varl1)
   1.535 -		end
   1.536 -            | compare_var_sides (_,_) = 
   1.537 -		locale_error ("Definitions must use the == relation")
   1.538 +    val err_var_rhs =
   1.539 +      let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) =
   1.540 +                let val varl1 = difflist d1 all_loc_consts;
   1.541 +                    val varl2 = difflist d2 all_loc_consts
   1.542 +                in t andalso (varl2 subset varl1)
   1.543 +                end
   1.544 +            | compare_var_sides (_,_) =
   1.545 +                locale_error ("Definitions must use the == relation")
   1.546            val check = Library.foldl compare_var_sides (true, loc_defs)
   1.547        in if check then []
   1.548           else ["nonfixed variable on right hand side of a locale definition in locale " ^ quote name]
   1.549 @@ -580,8 +567,8 @@
   1.550      else error (cat_lines errs);
   1.551  
   1.552      syntax_thy
   1.553 -    |> put_locale (name, 
   1.554 -		   make_locale ancestor loc_consts nosyn loc_thms_terms 
   1.555 +    |> put_locale (name,
   1.556 +                   make_locale ancestor loc_consts nosyn loc_thms_terms
   1.557                                          loc_defs_terms   loc_thms defaults)
   1.558    end;
   1.559  
   1.560 @@ -612,14 +599,14 @@
   1.561    | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
   1.562  
   1.563  (* pretty_term *)
   1.564 -fun pretty_term sign =
   1.565 -    if (is_open_loc_sg sign) then
   1.566 -        let val locale_list = map snd(get_scope_sg sign);
   1.567 +fun pretty_term thy =
   1.568 +    if (is_open_loc thy) then
   1.569 +        let val locale_list = map snd(get_scope thy);
   1.570              val nosyn = List.concat (map #nosyn locale_list);
   1.571 -            val str_list = (collect_consts sign) \\ nosyn
   1.572 -        in Sign.pretty_term sign o (const_ssubst_list str_list)
   1.573 +            val str_list = (collect_consts thy) \\ nosyn
   1.574 +        in Sign.pretty_term thy o (const_ssubst_list str_list)
   1.575          end
   1.576 -    else Sign.pretty_term sign;
   1.577 +    else Sign.pretty_term thy;
   1.578  
   1.579  
   1.580  
   1.581 @@ -644,10 +631,9 @@
   1.582  fun init_mkresult _ = error "No goal has been supplied in subgoal module";
   1.583  val curr_mkresult = ref (init_mkresult: bool*thm->thm);
   1.584  
   1.585 -val dummy = trivial(read_cterm (Theory.sign_of ProtoPure.thy)
   1.586 -    ("PROP No_goal_has_been_supplied",propT));
   1.587 +val dummy = Thm.trivial (read_cterm ProtoPure.thy ("PROP No_goal_has_been_supplied", propT));
   1.588  
   1.589 -(*List of previous goal stacks, for the undo operation.  Set by setstate. 
   1.590 +(*List of previous goal stacks, for the undo operation.  Set by setstate.
   1.591    A list of lists!*)
   1.592  val undo_list = ref([[(dummy, Seq.empty)]] : gstack list);
   1.593  
   1.594 @@ -662,9 +648,9 @@
   1.595  
   1.596  (*** Setting up goal-directed proof ***)
   1.597  
   1.598 -(*Generates the list of new theories when the proof state's signature changes*)
   1.599 -fun sign_error (sign,sign') =
   1.600 -  let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign
   1.601 +(*Generates the list of new theories when the proof state's theory changes*)
   1.602 +fun thy_error (thy,thy') =
   1.603 +  let val names = Context.names_of thy' \\ Context.names_of thy
   1.604    in  case names of
   1.605          [name] => "\nNew theory: " ^ name
   1.606        | _       => "\nNew theories: " ^ space_implode ", " names
   1.607 @@ -689,23 +675,22 @@
   1.608    end;
   1.609  
   1.610  (** exporting a theorem out of a locale means turning all meta-hyps into assumptions
   1.611 -    and expand and cancel the locale definitions. 
   1.612 +    and expand and cancel the locale definitions.
   1.613      export goes through all levels in case of nested locales, whereas
   1.614      export_thy just goes one up. **)
   1.615  
   1.616 -fun get_top_scope_thms thy = 
   1.617 -   let val sc = (get_scope_sg (Theory.sign_of thy))
   1.618 -   in if (null sc) then (warning "No locale in theory"; [])
   1.619 +fun get_top_scope_thms thy =
   1.620 +   let val sc = get_scope thy
   1.621 +   in if null sc then (warning "No locale in theory"; [])
   1.622        else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
   1.623     end;
   1.624  
   1.625 -fun implies_intr_some_hyps thy A_set th = 
   1.626 -   let 
   1.627 -       val sign = Theory.sign_of thy;
   1.628 +fun implies_intr_some_hyps thy A_set th =
   1.629 +   let
   1.630         val used_As = A_set inter #hyps(rep_thm(th));
   1.631 -       val ctl = map (cterm_of sign) used_As
   1.632 +       val ctl = map (cterm_of thy) used_As
   1.633     in Library.foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl)
   1.634 -   end; 
   1.635 +   end;
   1.636  
   1.637  fun standard_some thy A_set th =
   1.638    let val {maxidx,...} = rep_thm th
   1.639 @@ -716,7 +701,7 @@
   1.640         |> zero_var_indexes |> Thm.varifyT |> Thm.compress
   1.641    end;
   1.642  
   1.643 -fun export_thy thy th = 
   1.644 +fun export_thy thy th =
   1.645    let val A_set = get_top_scope_thms thy
   1.646    in
   1.647       standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th)))
   1.648 @@ -733,107 +718,106 @@
   1.649    "Goal::prop=>prop" to avoid assumptions being returned separately.
   1.650  *)
   1.651  fun prepare_proof atomic rths chorn =
   1.652 -  let val {sign, t=horn,...} = rep_cterm chorn;
   1.653 +  let val {thy, t=horn,...} = rep_cterm chorn;
   1.654        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
   1.655        val (As, B) = Logic.strip_horn horn;
   1.656        val atoms = atomic andalso
   1.657              forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
   1.658        val (As,B) = if atoms then ([],horn) else (As,B);
   1.659 -      val cAs = map (cterm_of sign) As;
   1.660 +      val cAs = map (cterm_of thy) As;
   1.661        val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
   1.662 -      val cB = cterm_of sign B;
   1.663 +      val cB = cterm_of thy B;
   1.664        val st0 = let val st = Drule.impose_hyps cAs (Drule.mk_triv_goal cB)
   1.665                  in  rewrite_goals_rule rths st end
   1.666        (*discharges assumptions from state in the order they appear in goal;
   1.667 -	checks (if requested) that resulting theorem is equivalent to goal. *)
   1.668 +        checks (if requested) that resulting theorem is equivalent to goal. *)
   1.669        fun mkresult (check,state) =
   1.670          let val state = Seq.hd (flexflex_rule state)
   1.671 -	    		handle THM _ => state   (*smash flexflex pairs*)
   1.672 -	    val ngoals = nprems_of state
   1.673 +                        handle THM _ => state   (*smash flexflex pairs*)
   1.674 +            val ngoals = nprems_of state
   1.675              val ath = implies_intr_list cAs state
   1.676              val th = ath RS Drule.rev_triv_goal
   1.677 -            val {hyps,prop,sign=sign',...} = rep_thm th
   1.678 +            val {hyps,prop,thy=thy',...} = rep_thm th
   1.679              val final_th = if (null(hyps)) then standard th else varify th
   1.680          in  if not check then final_th
   1.681 -	    else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state
   1.682 -		("Signature of proof state has changed!" ^
   1.683 -		 sign_error (sign,sign'))
   1.684 +            else if not (eq_thy(thy,thy')) then !result_error_fn state
   1.685 +                ("Theory of proof state has changed!" ^
   1.686 +                 thy_error (thy,thy'))
   1.687              else if ngoals>0 then !result_error_fn state
   1.688 -		(string_of_int ngoals ^ " unsolved goals!")
   1.689 -            else if (not (null hyps) andalso (not (in_locale hyps sign)))
   1.690 -		 then !result_error_fn state
   1.691 -                  ("Additional hypotheses:\n" ^ 
   1.692 -		   cat_lines 
   1.693 -		    (map (Sign.string_of_term sign) 
   1.694 -		     (List.filter (fn x => (not (in_locale [x] sign))) 
   1.695 -		      hyps)))
   1.696 -	    else if Pattern.matches (Sign.tsig_of sign)
   1.697 -			            (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   1.698 -		 then final_th
   1.699 -	    else  !result_error_fn state "proved a different theorem"
   1.700 +                (string_of_int ngoals ^ " unsolved goals!")
   1.701 +            else if (not (null hyps) andalso (not (in_locale hyps thy)))
   1.702 +                 then !result_error_fn state
   1.703 +                  ("Additional hypotheses:\n" ^
   1.704 +                   cat_lines
   1.705 +                    (map (Sign.string_of_term thy)
   1.706 +                     (List.filter (fn x => (not (in_locale [x] thy)))
   1.707 +                      hyps)))
   1.708 +            else if Pattern.matches (Sign.tsig_of thy)
   1.709 +                                    (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   1.710 +                 then final_th
   1.711 +            else  !result_error_fn state "proved a different theorem"
   1.712          end
   1.713    in
   1.714 -     if Sign.eq_sg(sign, Thm.sign_of_thm st0)
   1.715 +     if eq_thy(thy, Thm.theory_of_thm st0)
   1.716       then (prems, st0, mkresult)
   1.717 -     else error ("Definitions would change the proof state's signature" ^
   1.718 -		 sign_error (sign, Thm.sign_of_thm st0))
   1.719 +     else error ("Definitions would change the proof state's theory" ^
   1.720 +                 thy_error (thy, Thm.theory_of_thm st0))
   1.721    end
   1.722    handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
   1.723  
   1.724  (*Prints exceptions readably to users*)
   1.725 -fun print_sign_exn_unit sign e = 
   1.726 +fun print_sign_exn_unit thy e =
   1.727    case e of
   1.728       THM (msg,i,thms) =>
   1.729 -	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   1.730 -	  List.app print_thm thms)
   1.731 +         (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   1.732 +          List.app print_thm thms)
   1.733     | THEORY (msg,thys) =>
   1.734 -	 (writeln ("Exception THEORY raised:\n" ^ msg);
   1.735 -	  List.app (Pretty.writeln o Display.pretty_theory) thys)
   1.736 +         (writeln ("Exception THEORY raised:\n" ^ msg);
   1.737 +          List.app (writeln o Context.str_of_thy) thys)
   1.738     | TERM (msg,ts) =>
   1.739 -	 (writeln ("Exception TERM raised:\n" ^ msg);
   1.740 -	  List.app (writeln o Sign.string_of_term sign) ts)
   1.741 +         (writeln ("Exception TERM raised:\n" ^ msg);
   1.742 +          List.app (writeln o Sign.string_of_term thy) ts)
   1.743     | TYPE (msg,Ts,ts) =>
   1.744 -	 (writeln ("Exception TYPE raised:\n" ^ msg);
   1.745 -	  List.app (writeln o Sign.string_of_typ sign) Ts;
   1.746 -	  List.app (writeln o Sign.string_of_term sign) ts)
   1.747 +         (writeln ("Exception TYPE raised:\n" ^ msg);
   1.748 +          List.app (writeln o Sign.string_of_typ thy) Ts;
   1.749 +          List.app (writeln o Sign.string_of_term thy) ts)
   1.750     | e => raise e;
   1.751  
   1.752  (*Prints an exception, then fails*)
   1.753 -fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR);
   1.754 +fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR);
   1.755  
   1.756  (** the prove_goal.... commands
   1.757      Prove theorem using the listed tactics; check it has the specified form.
   1.758 -    Augment signature with all type assignments of goal.
   1.759 +    Augment theory with all type assignments of goal.
   1.760      Syntax is similar to "goal" command for easy keyboard use. **)
   1.761  
   1.762  (*Version taking the goal as a cterm*)
   1.763  fun prove_goalw_cterm_general check rths chorn tacsf =
   1.764    let val (prems, st0, mkresult) = prepare_proof false rths chorn
   1.765        val tac = EVERY (tacsf prems)
   1.766 -      fun statef() = 
   1.767 -	  (case Seq.pull (tac st0) of 
   1.768 -	       SOME(st,_) => st
   1.769 -	     | _ => error ("prove_goal: tactic failed"))
   1.770 +      fun statef() =
   1.771 +          (case Seq.pull (tac st0) of
   1.772 +               SOME(st,_) => st
   1.773 +             | _ => error ("prove_goal: tactic failed"))
   1.774    in  mkresult (check, cond_timeit (!Output.timing) statef)  end
   1.775 -  handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e;
   1.776 -	       writeln ("The exception above was raised for\n" ^ 
   1.777 -		      Display.string_of_cterm chorn); raise e);
   1.778 +  handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
   1.779 +               writeln ("The exception above was raised for\n" ^
   1.780 +                      Display.string_of_cterm chorn); raise e);
   1.781  
   1.782 -(*Two variants: one checking the result, one not.  
   1.783 +(*Two variants: one checking the result, one not.
   1.784    Neither prints runtime messages: they are for internal packages.*)
   1.785 -fun prove_goalw_cterm rths chorn = 
   1.786 -	setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
   1.787 -and prove_goalw_cterm_nocheck rths chorn = 
   1.788 -	setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
   1.789 +fun prove_goalw_cterm rths chorn =
   1.790 +        setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
   1.791 +and prove_goalw_cterm_nocheck rths chorn =
   1.792 +        setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
   1.793  
   1.794  
   1.795  (*Version taking the goal as a string*)
   1.796  fun prove_goalw thy rths agoal tacsf =
   1.797 -  let val sign = Theory.sign_of thy
   1.798 -      val chorn = read_cterm sign (agoal,propT)
   1.799 -  in  prove_goalw_cterm_general true rths chorn tacsf end
   1.800 +  let val chorn = read_cterm thy (agoal, propT)
   1.801 +  in prove_goalw_cterm_general true rths chorn tacsf end
   1.802    handle ERROR => error (*from read_cterm?*)
   1.803 -		("The error(s) above occurred for " ^ quote agoal);
   1.804 +                ("The error(s) above occurred for " ^ quote agoal);
   1.805  
   1.806  (*String version with no meta-rewrite-rules*)
   1.807  fun prove_goal thy = prove_goalw thy [];
   1.808 @@ -847,7 +831,7 @@
   1.809  (*** Commands etc ***)
   1.810  
   1.811  (*Return the current goal stack, if any, from undo_list*)
   1.812 -fun getstate() : gstack = case !undo_list of 
   1.813 +fun getstate() : gstack = case !undo_list of
   1.814        []   => error"No current state in subgoal module"
   1.815      | x::_ => x;
   1.816  
   1.817 @@ -868,7 +852,7 @@
   1.818  
   1.819  (*Printing can raise exceptions, so the assignment occurs last.
   1.820    Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
   1.821 -fun setstate newgoals = 
   1.822 +fun setstate newgoals =
   1.823    (print_top (pop newgoals);  undo_list := newgoals :: !undo_list);
   1.824  
   1.825  (*Given a proof state transformation, return a command that updates
   1.826 @@ -895,7 +879,7 @@
   1.827    For debugging uses of METAHYPS*)
   1.828  local exception GETHYPS of thm list
   1.829  in
   1.830 -fun gethyps i = 
   1.831 +fun gethyps i =
   1.832      (METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm());  [])
   1.833      handle GETHYPS hyps => hyps
   1.834  end;
   1.835 @@ -904,14 +888,14 @@
   1.836  fun filter_goal could ths i = filter_thms could (999, getgoal i, ths);
   1.837  
   1.838  (*For inspecting earlier levels of the backward proof*)
   1.839 -fun chop_level n (pair,pairs) = 
   1.840 +fun chop_level n (pair,pairs) =
   1.841    let val level = length pairs
   1.842    in  if n<0 andalso ~n <= level
   1.843 -      then  List.drop (pair::pairs, ~n) 
   1.844 +      then  List.drop (pair::pairs, ~n)
   1.845        else if 0<=n andalso n<= level
   1.846 -      then  List.drop (pair::pairs, level - n) 
   1.847 -      else  error ("Level number must lie between 0 and " ^ 
   1.848 -		   string_of_int level)
   1.849 +      then  List.drop (pair::pairs, level - n)
   1.850 +      else  error ("Level number must lie between 0 and " ^
   1.851 +                   string_of_int level)
   1.852    end;
   1.853  
   1.854  (*Print the given level of the proof; prlev ~1 prints previous level*)
   1.855 @@ -922,15 +906,15 @@
   1.856  fun prlim n = (goals_limit:=n; pr());
   1.857  
   1.858  (** the goal.... commands
   1.859 -    Read main goal.  Set global variables curr_prems, curr_mkresult. 
   1.860 +    Read main goal.  Set global variables curr_prems, curr_mkresult.
   1.861      Initial subgoal and premises are rewritten using rths. **)
   1.862  
   1.863  (*Version taking the goal as a cterm; if you have a term t and theory thy, use
   1.864 -    goalw_cterm rths (cterm_of (Theory.sign_of thy) t);      *)
   1.865 -fun agoalw_cterm atomic rths chorn = 
   1.866 +    goalw_cterm rths (cterm_of thy t);      *)
   1.867 +fun agoalw_cterm atomic rths chorn =
   1.868    let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
   1.869    in  undo_list := [];
   1.870 -      setstate [ (st0, Seq.empty) ];  
   1.871 +      setstate [ (st0, Seq.empty) ];
   1.872        curr_prems := prems;
   1.873        curr_mkresult := mkresult;
   1.874        prems
   1.875 @@ -939,10 +923,10 @@
   1.876  val goalw_cterm = agoalw_cterm false;
   1.877  
   1.878  (*Version taking the goal as a string*)
   1.879 -fun agoalw atomic thy rths agoal = 
   1.880 -    agoalw_cterm atomic rths (read_cterm(Theory.sign_of thy)(agoal,propT))
   1.881 +fun agoalw atomic thy rths agoal =
   1.882 +    agoalw_cterm atomic rths (read_cterm thy (agoal, propT))
   1.883      handle ERROR => error (*from type_assign, etc via prepare_proof*)
   1.884 -	("The error(s) above occurred for " ^ quote agoal);
   1.885 +        ("The error(s) above occurred for " ^ quote agoal);
   1.886  
   1.887  val goalw = agoalw false;
   1.888  
   1.889 @@ -978,15 +962,15 @@
   1.890  fun by_com tac ((th,ths), pairs) : gstack =
   1.891    (case  Seq.pull(tac th)  of
   1.892       NONE      => error"by: tactic failed"
   1.893 -   | SOME(th2,ths2) => 
   1.894 -       (if eq_thm(th,th2) 
   1.895 -	  then warning "Warning: same as previous level"
   1.896 -	  else if eq_thm_sg(th,th2) then ()
   1.897 -	  else warning ("Warning: signature of proof state has changed" ^
   1.898 -		       sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
   1.899 +   | SOME(th2,ths2) =>
   1.900 +       (if eq_thm(th,th2)
   1.901 +          then warning "Warning: same as previous level"
   1.902 +          else if eq_thm_thy(th,th2) then ()
   1.903 +          else warning ("Warning: theory of proof state has changed" ^
   1.904 +                       thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
   1.905         ((th2,ths2)::(th,ths)::pairs)));
   1.906  
   1.907 -fun by tac = cond_timeit (!Output.timing) 
   1.908 +fun by tac = cond_timeit (!Output.timing)
   1.909      (fn() => make_command (by_com tac));
   1.910  
   1.911  (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.
   1.912 @@ -999,13 +983,13 @@
   1.913  fun backtrack [] = error"back: no alternatives"
   1.914    | backtrack ((th,thstr) :: pairs) =
   1.915       (case Seq.pull thstr of
   1.916 -	  NONE      => (writeln"Going back a level..."; backtrack pairs)
   1.917 -	| SOME(th2,thstr2) =>  
   1.918 -	   (if eq_thm(th,th2) 
   1.919 -	      then warning "Warning: same as previous choice at this level"
   1.920 -	      else if eq_thm_sg(th,th2) then ()
   1.921 -	      else warning "Warning: signature of proof state has changed";
   1.922 -	    (th2,thstr2)::pairs));
   1.923 +          NONE      => (writeln"Going back a level..."; backtrack pairs)
   1.924 +        | SOME(th2,thstr2) =>
   1.925 +           (if eq_thm(th,th2)
   1.926 +              then warning "Warning: same as previous choice at this level"
   1.927 +              else if eq_thm_thy(th,th2) then ()
   1.928 +              else warning "Warning: theory of proof state has changed";
   1.929 +            (th2,thstr2)::pairs));
   1.930  
   1.931  fun back() = setstate (backtrack (getstate()));
   1.932  
   1.933 @@ -1031,25 +1015,25 @@
   1.934  
   1.935  
   1.936  fun top_proof() = case !proofstack of
   1.937 -	[] => error("Stack of proof attempts is empty!")
   1.938 +        [] => error("Stack of proof attempts is empty!")
   1.939      | p::ps => (p,ps);
   1.940  
   1.941  (*  push a copy of the current proof state on to the stack *)
   1.942  fun push_proof() = (proofstack := (save_proof() :: !proofstack));
   1.943  
   1.944  (* discard the top proof state of the stack *)
   1.945 -fun pop_proof() = 
   1.946 +fun pop_proof() =
   1.947    let val (p,ps) = top_proof()
   1.948        val prems = restore_proof p
   1.949    in proofstack := ps;  pr();  prems end;
   1.950  
   1.951  (* rotate the stack so that the top element goes to the bottom *)
   1.952  fun rotate_proof() = let val (p,ps) = top_proof()
   1.953 -		    in proofstack := ps@[save_proof()];
   1.954 -		       restore_proof p;
   1.955 -		       pr();
   1.956 -		       !curr_prems
   1.957 -		    end;
   1.958 +                    in proofstack := ps@[save_proof()];
   1.959 +                       restore_proof p;
   1.960 +                       pr();
   1.961 +                       !curr_prems
   1.962 +                    end;
   1.963  
   1.964  
   1.965  (** Shortcuts for commonly-used tactics **)
   1.966 @@ -1085,11 +1069,11 @@
   1.967  
   1.968  (** Reading and printing terms wrt the current theory **)
   1.969  
   1.970 -fun top_sg() = Thm.sign_of_thm (topthm());
   1.971 +fun top_sg() = Thm.theory_of_thm (topthm());
   1.972  
   1.973  fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
   1.974  
   1.975 -(*Print a term under the current signature of the proof state*)
   1.976 +(*Print a term under the current theory of the proof state*)
   1.977  fun prin t = writeln (Sign.string_of_term (top_sg()) t);
   1.978  
   1.979  fun printyp T = writeln (Sign.string_of_typ (top_sg()) T);
   1.980 @@ -1099,7 +1083,7 @@
   1.981  fun pprint_typ T = Sign.pprint_typ (top_sg()) T;
   1.982  
   1.983  
   1.984 -(*Prints exceptions nicely at top level; 
   1.985 +(*Prints exceptions nicely at top level;
   1.986    raises the exception in order to have a polymorphic type!*)
   1.987  fun print_exn e = (print_sign_exn_unit (top_sg()) e;  raise e);
   1.988  
   1.989 @@ -1128,15 +1112,15 @@
   1.990  
   1.991  (* retrieval *)
   1.992  
   1.993 -fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (topthm ()));
   1.994 +fun theory_of_goal () = Thm.theory_of_thm (topthm ());
   1.995  val context_of_goal = ProofContext.init o theory_of_goal;
   1.996  
   1.997  fun thms_containing raw_consts =
   1.998    let
   1.999      val thy = theory_of_goal ();
  1.1000 -    val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
  1.1001 +    val consts = map (Sign.intern_const thy) raw_consts;
  1.1002    in
  1.1003 -    (case List.filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
  1.1004 +    (case List.filter (is_none o Sign.const_type thy) consts of
  1.1005        [] => ()
  1.1006      | cs => error ("thms_containing: undeclared consts " ^ commas_quote cs));
  1.1007      PureThy.thms_containing_consts thy consts