rep_cterm/rep_thm: no longer dereference theory_ref;
authorwenzelm
Sat Apr 12 17:00:35 2008 +0200 (2008-04-12)
changeset 26626c6231d64d264
parent 26625 e0cc4169626e
child 26627 dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record_package.ML
src/HOLCF/Tools/adm_tac.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/codegen.ML
src/Pure/display.ML
src/Pure/meta_simplifier.ML
src/Pure/old_goals.ML
src/Pure/pure_thy.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Apr 10 20:54:18 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Apr 12 17:00:35 2008 +0200
     1.3 @@ -13,42 +13,42 @@
     1.4  
     1.5      type proof_info
     1.6      datatype proof = Proof of proof_info * proof_content
     1.7 -	 and proof_content
     1.8 -	   = PRefl of term
     1.9 -	   | PInstT of proof * (hol_type,hol_type) subst
    1.10 -	   | PSubst of proof list * term * proof
    1.11 -	   | PAbs of proof * term
    1.12 -	   | PDisch of proof * term
    1.13 -	   | PMp of proof * proof
    1.14 -	   | PHyp of term
    1.15 -	   | PAxm of string * term
    1.16 -	   | PDef of string * string * term
    1.17 -	   | PTmSpec of string * string list * proof
    1.18 -	   | PTyDef of string * string * proof
    1.19 -	   | PTyIntro of string * string * string * string * term * term * proof
    1.20 -	   | POracle of tag * term list * term
    1.21 -	   | PDisk
    1.22 -	   | PSpec of proof * term
    1.23 -	   | PInst of proof * (term,term) subst
    1.24 -	   | PGen of proof * term
    1.25 -	   | PGenAbs of proof * term option * term list
    1.26 -	   | PImpAS of proof * proof
    1.27 -	   | PSym of proof
    1.28 -	   | PTrans of proof * proof
    1.29 -	   | PComb of proof * proof
    1.30 -	   | PEqMp of proof * proof
    1.31 -	   | PEqImp of proof
    1.32 -	   | PExists of proof * term * term
    1.33 -	   | PChoose of term * proof * proof
    1.34 -	   | PConj of proof * proof
    1.35 -	   | PConjunct1 of proof
    1.36 -	   | PConjunct2 of proof
    1.37 -	   | PDisj1 of proof * term
    1.38 -	   | PDisj2 of proof * term
    1.39 -	   | PDisjCases of proof * proof * proof
    1.40 -	   | PNotI of proof
    1.41 -	   | PNotE of proof
    1.42 -	   | PContr of proof * term
    1.43 +         and proof_content
    1.44 +           = PRefl of term
    1.45 +           | PInstT of proof * (hol_type,hol_type) subst
    1.46 +           | PSubst of proof list * term * proof
    1.47 +           | PAbs of proof * term
    1.48 +           | PDisch of proof * term
    1.49 +           | PMp of proof * proof
    1.50 +           | PHyp of term
    1.51 +           | PAxm of string * term
    1.52 +           | PDef of string * string * term
    1.53 +           | PTmSpec of string * string list * proof
    1.54 +           | PTyDef of string * string * proof
    1.55 +           | PTyIntro of string * string * string * string * term * term * proof
    1.56 +           | POracle of tag * term list * term
    1.57 +           | PDisk
    1.58 +           | PSpec of proof * term
    1.59 +           | PInst of proof * (term,term) subst
    1.60 +           | PGen of proof * term
    1.61 +           | PGenAbs of proof * term option * term list
    1.62 +           | PImpAS of proof * proof
    1.63 +           | PSym of proof
    1.64 +           | PTrans of proof * proof
    1.65 +           | PComb of proof * proof
    1.66 +           | PEqMp of proof * proof
    1.67 +           | PEqImp of proof
    1.68 +           | PExists of proof * term * term
    1.69 +           | PChoose of term * proof * proof
    1.70 +           | PConj of proof * proof
    1.71 +           | PConjunct1 of proof
    1.72 +           | PConjunct2 of proof
    1.73 +           | PDisj1 of proof * term
    1.74 +           | PDisj2 of proof * term
    1.75 +           | PDisjCases of proof * proof * proof
    1.76 +           | PNotI of proof
    1.77 +           | PNotE of proof
    1.78 +           | PContr of proof * term
    1.79  
    1.80      exception PK of string * string
    1.81  
    1.82 @@ -178,7 +178,7 @@
    1.83  
    1.84  fun print_exn e =
    1.85      case e of
    1.86 -	PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
    1.87 +        PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
    1.88        | _ => OldGoals.print_exn e
    1.89  
    1.90  (* Compatibility. *)
    1.91 @@ -194,47 +194,49 @@
    1.92  
    1.93  fun simple_smart_string_of_cterm ct =
    1.94      let
    1.95 -	val {thy,t,T,...} = rep_cterm ct
    1.96 -	(* Hack to avoid parse errors with Trueprop *)
    1.97 -	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    1.98 -			   handle TERM _ => ct)
    1.99 +        val thy = Thm.theory_of_cterm ct;
   1.100 +        val {t,T,...} = rep_cterm ct
   1.101 +        (* Hack to avoid parse errors with Trueprop *)
   1.102 +        val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
   1.103 +                           handle TERM _ => ct)
   1.104      in
   1.105 -	quote(
   1.106 -	PrintMode.setmp [] (
   1.107 -	Library.setmp show_brackets false (
   1.108 -	Library.setmp show_all_types true (
   1.109 -	Library.setmp Syntax.ambiguity_is_error false (
   1.110 -	Library.setmp show_sorts true string_of_cterm))))
   1.111 -	ct)
   1.112 +        quote(
   1.113 +        PrintMode.setmp [] (
   1.114 +        Library.setmp show_brackets false (
   1.115 +        Library.setmp show_all_types true (
   1.116 +        Library.setmp Syntax.ambiguity_is_error false (
   1.117 +        Library.setmp show_sorts true string_of_cterm))))
   1.118 +        ct)
   1.119      end
   1.120  
   1.121  exception SMART_STRING
   1.122  
   1.123  fun smart_string_of_cterm ct =
   1.124      let
   1.125 -	val {thy,t,T,...} = rep_cterm ct
   1.126 +        val thy = Thm.theory_of_cterm ct
   1.127          val ctxt = ProofContext.init thy
   1.128 +        val {t,T,...} = rep_cterm ct
   1.129          (* Hack to avoid parse errors with Trueprop *)
   1.130 -	val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
   1.131 -		   handle TERM _ => ct)
   1.132 -	fun match u = t aconv u
   1.133 -	fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
   1.134 -	  | G 1 = Library.setmp show_brackets true (G 0)
   1.135 -	  | G 2 = Library.setmp show_all_types true (G 0)
   1.136 -	  | G 3 = Library.setmp show_brackets true (G 2)
   1.137 +        val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
   1.138 +                   handle TERM _ => ct)
   1.139 +        fun match u = t aconv u
   1.140 +        fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
   1.141 +          | G 1 = Library.setmp show_brackets true (G 0)
   1.142 +          | G 2 = Library.setmp show_all_types true (G 0)
   1.143 +          | G 3 = Library.setmp show_brackets true (G 2)
   1.144            | G _ = raise SMART_STRING
   1.145 -	fun F n =
   1.146 -	    let
   1.147 -		val str = Library.setmp show_brackets false (G n string_of_cterm) ct
   1.148 -		val u = Syntax.parse_term ctxt str
   1.149 +        fun F n =
   1.150 +            let
   1.151 +                val str = Library.setmp show_brackets false (G n string_of_cterm) ct
   1.152 +                val u = Syntax.parse_term ctxt str
   1.153                    |> TypeInfer.constrain T |> Syntax.check_term ctxt
   1.154 -	    in
   1.155 -		if match u
   1.156 -		then quote str
   1.157 -		else F (n+1)
   1.158 -	    end
   1.159 -	    handle ERROR mesg => F (n+1)
   1.160 -		 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
   1.161 +            in
   1.162 +                if match u
   1.163 +                then quote str
   1.164 +                else F (n+1)
   1.165 +            end
   1.166 +            handle ERROR mesg => F (n+1)
   1.167 +                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
   1.168      in
   1.169        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
   1.170      end
   1.171 @@ -247,11 +249,11 @@
   1.172  fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
   1.173  fun pth (HOLThm(ren,thm)) =
   1.174      let
   1.175 -	(*val _ = writeln "Renaming:"
   1.176 -	val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
   1.177 -	val _ = prth thm
   1.178 +        (*val _ = writeln "Renaming:"
   1.179 +        val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
   1.180 +        val _ = prth thm
   1.181      in
   1.182 -	()
   1.183 +        ()
   1.184      end
   1.185  
   1.186  fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info
   1.187 @@ -267,16 +269,16 @@
   1.188  
   1.189  fun assoc x =
   1.190      let
   1.191 -	fun F [] = raise PK("Lib.assoc","Not found")
   1.192 -	  | F ((x',y)::rest) = if x = x'
   1.193 -			       then y
   1.194 -			       else F rest
   1.195 +        fun F [] = raise PK("Lib.assoc","Not found")
   1.196 +          | F ((x',y)::rest) = if x = x'
   1.197 +                               then y
   1.198 +                               else F rest
   1.199      in
   1.200 -	F
   1.201 +        F
   1.202      end
   1.203  fun i mem L =
   1.204      let fun itr [] = false
   1.205 -	  | itr (a::rst) = i=a orelse itr rst
   1.206 +          | itr (a::rst) = i=a orelse itr rst
   1.207      in itr L end;
   1.208  
   1.209  fun insert i L = if i mem L then L else i::L
   1.210 @@ -305,7 +307,7 @@
   1.211  (* Actual code. *)
   1.212  
   1.213  fun get_segment thyname l = (Lib.assoc "s" l
   1.214 -			     handle PK _ => thyname)
   1.215 +                             handle PK _ => thyname)
   1.216  val get_name : (string * string) list -> string = Lib.assoc "n"
   1.217  
   1.218  local
   1.219 @@ -333,43 +335,43 @@
   1.220  
   1.221  fun scan_string str c =
   1.222      let
   1.223 -	fun F [] toks = (c,toks)
   1.224 -	  | F (c::cs) toks =
   1.225 -	    case LazySeq.getItem toks of
   1.226 -		SOME(c',toks') =>
   1.227 -		if c = c'
   1.228 -		then F cs toks'
   1.229 -		else raise SyntaxError
   1.230 -	      | NONE => raise SyntaxError
   1.231 +        fun F [] toks = (c,toks)
   1.232 +          | F (c::cs) toks =
   1.233 +            case LazySeq.getItem toks of
   1.234 +                SOME(c',toks') =>
   1.235 +                if c = c'
   1.236 +                then F cs toks'
   1.237 +                else raise SyntaxError
   1.238 +              | NONE => raise SyntaxError
   1.239      in
   1.240 -	F (String.explode str)
   1.241 +        F (String.explode str)
   1.242      end
   1.243  
   1.244  local
   1.245      val scan_entity =
   1.246 -	(scan_string "amp;" #"&")
   1.247 -	    || scan_string "quot;" #"\""
   1.248 -	    || scan_string "gt;" #">"
   1.249 -	    || scan_string "lt;" #"<"
   1.250 +        (scan_string "amp;" #"&")
   1.251 +            || scan_string "quot;" #"\""
   1.252 +            || scan_string "gt;" #">"
   1.253 +            || scan_string "lt;" #"<"
   1.254              || scan_string "apos;" #"'"
   1.255  in
   1.256  fun scan_nonquote toks =
   1.257      case LazySeq.getItem toks of
   1.258 -	SOME (c,toks') =>
   1.259 -	(case c of
   1.260 -	     #"\"" => raise SyntaxError
   1.261 -	   | #"&" => scan_entity toks'
   1.262 -	   | c => (c,toks'))
   1.263 +        SOME (c,toks') =>
   1.264 +        (case c of
   1.265 +             #"\"" => raise SyntaxError
   1.266 +           | #"&" => scan_entity toks'
   1.267 +           | c => (c,toks'))
   1.268        | NONE => raise SyntaxError
   1.269  end
   1.270  
   1.271  val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >>
   1.272 -		     String.implode
   1.273 +                     String.implode
   1.274  
   1.275  val scan_attribute = scan_id -- $$ #"=" |-- scan_string
   1.276  
   1.277  val scan_start_of_tag = $$ #"<" |-- scan_id --
   1.278 -			   repeat ($$ #" " |-- scan_attribute)
   1.279 +                           repeat ($$ #" " |-- scan_attribute)
   1.280  
   1.281  (* The evaluation delay introduced through the 'toks' argument is needed
   1.282  for the sake of the SML/NJ (110.9.1) compiler.  Either that or an explicit
   1.283 @@ -379,15 +381,15 @@
   1.284  val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
   1.285  
   1.286  fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
   1.287 -		       (fn (chldr,id') => if id = id'
   1.288 -					  then chldr
   1.289 -					  else raise XML "Tag mismatch")
   1.290 +                       (fn (chldr,id') => if id = id'
   1.291 +                                          then chldr
   1.292 +                                          else raise XML "Tag mismatch")
   1.293  and scan_tag toks =
   1.294      let
   1.295 -	val ((id,atts),toks2) = scan_start_of_tag toks
   1.296 -	val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
   1.297 +        val ((id,atts),toks2) = scan_start_of_tag toks
   1.298 +        val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
   1.299      in
   1.300 -	(Elem (id,atts,chldr),toks3)
   1.301 +        (Elem (id,atts,chldr),toks3)
   1.302      end
   1.303  end
   1.304  
   1.305 @@ -398,28 +400,28 @@
   1.306  
   1.307  fun mk_defeq name rhs thy =
   1.308      let
   1.309 -	val ty = type_of rhs
   1.310 +        val ty = type_of rhs
   1.311      in
   1.312 -	Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs)
   1.313 +        Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs)
   1.314      end
   1.315  
   1.316  fun mk_teq name rhs thy =
   1.317      let
   1.318 -	val ty = type_of rhs
   1.319 +        val ty = type_of rhs
   1.320      in
   1.321 -	HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs)
   1.322 +        HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs)
   1.323      end
   1.324  
   1.325  fun intern_const_name thyname const thy =
   1.326      case get_hol4_const_mapping thyname const thy of
   1.327 -	SOME (_,cname,_) => cname
   1.328 +        SOME (_,cname,_) => cname
   1.329        | NONE => (case get_hol4_const_renaming thyname const thy of
   1.330 -		     SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
   1.331 -		   | NONE => Sign.intern_const thy (thyname ^ "." ^ const))
   1.332 +                     SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
   1.333 +                   | NONE => Sign.intern_const thy (thyname ^ "." ^ const))
   1.334  
   1.335  fun intern_type_name thyname const thy =
   1.336      case get_hol4_type_mapping thyname const thy of
   1.337 -	SOME (_,cname) => cname
   1.338 +        SOME (_,cname) => cname
   1.339        | NONE => Sign.intern_const thy (thyname ^ "." ^ const)
   1.340  
   1.341  fun mk_vartype name = TFree(name,["HOL.type"])
   1.342 @@ -454,16 +456,16 @@
   1.343  (* Needed for HOL Light *)
   1.344  fun protect_tyvarname s =
   1.345      let
   1.346 -	fun no_quest s =
   1.347 -	    if Char.contains s #"?"
   1.348 -	    then String.translate (fn #"?" => "q_" | c => Char.toString c) s
   1.349 -	    else s
   1.350 -	fun beg_prime s =
   1.351 -	    if String.isPrefix "'" s
   1.352 -	    then s
   1.353 -	    else "'" ^ s
   1.354 +        fun no_quest s =
   1.355 +            if Char.contains s #"?"
   1.356 +            then String.translate (fn #"?" => "q_" | c => Char.toString c) s
   1.357 +            else s
   1.358 +        fun beg_prime s =
   1.359 +            if String.isPrefix "'" s
   1.360 +            then s
   1.361 +            else "'" ^ s
   1.362      in
   1.363 -	s |> no_quest |> beg_prime
   1.364 +        s |> no_quest |> beg_prime
   1.365      end
   1.366  
   1.367  val protected_varnames = ref (Symtab.empty:string Symtab.table)
   1.368 @@ -485,26 +487,26 @@
   1.369        SOME t => t
   1.370      | NONE =>
   1.371        let
   1.372 -	  val _ = inc invented_isavar
   1.373 -	  val t = "u_" ^ string_of_int (!invented_isavar)
   1.374 -	  val _ = ImportRecorder.protect_varname s t
   1.375 +          val _ = inc invented_isavar
   1.376 +          val t = "u_" ^ string_of_int (!invented_isavar)
   1.377 +          val _ = ImportRecorder.protect_varname s t
   1.378            val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   1.379        in
   1.380 -	  t
   1.381 +          t
   1.382        end
   1.383  
   1.384  exception REPLAY_PROTECT_VARNAME of string*string*string
   1.385  
   1.386  fun replay_protect_varname s t =
   1.387 -	case Symtab.lookup (!protected_varnames) s of
   1.388 -	  SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
   1.389 -	| NONE =>
   1.390 +        case Symtab.lookup (!protected_varnames) s of
   1.391 +          SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
   1.392 +        | NONE =>
   1.393            let
   1.394 -	      val _ = inc invented_isavar
   1.395 -	      val t = "u_" ^ string_of_int (!invented_isavar)
   1.396 +              val _ = inc invented_isavar
   1.397 +              val t = "u_" ^ string_of_int (!invented_isavar)
   1.398                val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   1.399            in
   1.400 -	      ()
   1.401 +              ()
   1.402            end
   1.403  
   1.404  fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
   1.405 @@ -554,46 +556,46 @@
   1.406  
   1.407  fun get_type_from_index thy thyname types is =
   1.408      case Int.fromString is of
   1.409 -	SOME i => (case Array.sub(types,i) of
   1.410 -		       FullType ty => ty
   1.411 -		     | XMLty xty =>
   1.412 -		       let
   1.413 -			   val ty = get_type_from_xml thy thyname types xty
   1.414 -			   val _  = Array.update(types,i,FullType ty)
   1.415 -		       in
   1.416 -			   ty
   1.417 -		       end)
   1.418 +        SOME i => (case Array.sub(types,i) of
   1.419 +                       FullType ty => ty
   1.420 +                     | XMLty xty =>
   1.421 +                       let
   1.422 +                           val ty = get_type_from_xml thy thyname types xty
   1.423 +                           val _  = Array.update(types,i,FullType ty)
   1.424 +                       in
   1.425 +                           ty
   1.426 +                       end)
   1.427        | NONE => raise ERR "get_type_from_index" "Bad index"
   1.428  and get_type_from_xml thy thyname types =
   1.429      let
   1.430 -	fun gtfx (Elem("tyi",[("i",iS)],[])) =
   1.431 -		 get_type_from_index thy thyname types iS
   1.432 -	  | gtfx (Elem("tyc",atts,[])) =
   1.433 -	    mk_thy_type thy
   1.434 -			(get_segment thyname atts)
   1.435 -			(protect_tyname (get_name atts))
   1.436 -			[]
   1.437 -	  | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s)
   1.438 -	  | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) =
   1.439 -	    mk_thy_type thy
   1.440 -			(get_segment thyname atts)
   1.441 -			(protect_tyname (get_name atts))
   1.442 -			(map gtfx tys)
   1.443 -	  | gtfx _ = raise ERR "get_type" "Bad type"
   1.444 +        fun gtfx (Elem("tyi",[("i",iS)],[])) =
   1.445 +                 get_type_from_index thy thyname types iS
   1.446 +          | gtfx (Elem("tyc",atts,[])) =
   1.447 +            mk_thy_type thy
   1.448 +                        (get_segment thyname atts)
   1.449 +                        (protect_tyname (get_name atts))
   1.450 +                        []
   1.451 +          | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s)
   1.452 +          | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) =
   1.453 +            mk_thy_type thy
   1.454 +                        (get_segment thyname atts)
   1.455 +                        (protect_tyname (get_name atts))
   1.456 +                        (map gtfx tys)
   1.457 +          | gtfx _ = raise ERR "get_type" "Bad type"
   1.458      in
   1.459 -	gtfx
   1.460 +        gtfx
   1.461      end
   1.462  
   1.463  fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
   1.464      let
   1.465 -	val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
   1.466 -	fun IT _ [] = ()
   1.467 -	  | IT n (xty::xtys) =
   1.468 -	    (Array.update(types,n,XMLty xty);
   1.469 -	     IT (n+1) xtys)
   1.470 -	val _ = IT 0 xtys
   1.471 +        val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
   1.472 +        fun IT _ [] = ()
   1.473 +          | IT n (xty::xtys) =
   1.474 +            (Array.update(types,n,XMLty xty);
   1.475 +             IT (n+1) xtys)
   1.476 +        val _ = IT 0 xtys
   1.477      in
   1.478 -	types
   1.479 +        types
   1.480      end
   1.481    | input_types _ _ = raise ERR "input_types" "Bad type list"
   1.482  end
   1.483 @@ -603,392 +605,392 @@
   1.484  
   1.485  fun get_term_from_index thy thyname types terms is =
   1.486      case Int.fromString is of
   1.487 -	SOME i => (case Array.sub(terms,i) of
   1.488 -		       FullTerm tm => tm
   1.489 -		     | XMLtm xtm =>
   1.490 -		       let
   1.491 -			   val tm = get_term_from_xml thy thyname types terms xtm
   1.492 -			   val _  = Array.update(terms,i,FullTerm tm)
   1.493 -		       in
   1.494 -			   tm
   1.495 -		       end)
   1.496 +        SOME i => (case Array.sub(terms,i) of
   1.497 +                       FullTerm tm => tm
   1.498 +                     | XMLtm xtm =>
   1.499 +                       let
   1.500 +                           val tm = get_term_from_xml thy thyname types terms xtm
   1.501 +                           val _  = Array.update(terms,i,FullTerm tm)
   1.502 +                       in
   1.503 +                           tm
   1.504 +                       end)
   1.505        | NONE => raise ERR "get_term_from_index" "Bad index"
   1.506  and get_term_from_xml thy thyname types terms =
   1.507      let
   1.508 -	fun get_type [] = NONE
   1.509 -	  | get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty)
   1.510 -	  | get_type _ = raise ERR "get_term" "Bad type"
   1.511 +        fun get_type [] = NONE
   1.512 +          | get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty)
   1.513 +          | get_type _ = raise ERR "get_term" "Bad type"
   1.514  
   1.515 -	fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) =
   1.516 -	    mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi)
   1.517 -	  | gtfx (Elem("tmc",atts,[])) =
   1.518 -	    let
   1.519 -		val segment = get_segment thyname atts
   1.520 -		val name = protect_constname(get_name atts)
   1.521 -	    in
   1.522 -		mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
   1.523 -		handle PK _ => prim_mk_const thy segment name
   1.524 -	    end
   1.525 -	  | gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) =
   1.526 -	    let
   1.527 -		val f = get_term_from_index thy thyname types terms tmf
   1.528 -		val a = get_term_from_index thy thyname types terms tma
   1.529 -	    in
   1.530 -		mk_comb(f,a)
   1.531 -	    end
   1.532 -	  | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
   1.533 -	    let
   1.534 +        fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) =
   1.535 +            mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi)
   1.536 +          | gtfx (Elem("tmc",atts,[])) =
   1.537 +            let
   1.538 +                val segment = get_segment thyname atts
   1.539 +                val name = protect_constname(get_name atts)
   1.540 +            in
   1.541 +                mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
   1.542 +                handle PK _ => prim_mk_const thy segment name
   1.543 +            end
   1.544 +          | gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) =
   1.545 +            let
   1.546 +                val f = get_term_from_index thy thyname types terms tmf
   1.547 +                val a = get_term_from_index thy thyname types terms tma
   1.548 +            in
   1.549 +                mk_comb(f,a)
   1.550 +            end
   1.551 +          | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
   1.552 +            let
   1.553                  val x = get_term_from_index thy thyname types terms tmx
   1.554                  val a = get_term_from_index thy thyname types terms tma
   1.555 -	    in
   1.556 -		mk_lambda x a
   1.557 -	    end
   1.558 -	  | gtfx (Elem("tmi",[("i",iS)],[])) =
   1.559 -	    get_term_from_index thy thyname types terms iS
   1.560 -	  | gtfx (Elem(tag,_,_)) =
   1.561 -	    raise ERR "get_term" ("Not a term: "^tag)
   1.562 +            in
   1.563 +                mk_lambda x a
   1.564 +            end
   1.565 +          | gtfx (Elem("tmi",[("i",iS)],[])) =
   1.566 +            get_term_from_index thy thyname types terms iS
   1.567 +          | gtfx (Elem(tag,_,_)) =
   1.568 +            raise ERR "get_term" ("Not a term: "^tag)
   1.569      in
   1.570 -	gtfx
   1.571 +        gtfx
   1.572      end
   1.573  
   1.574  fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
   1.575      let
   1.576 -	val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
   1.577 +        val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
   1.578  
   1.579 -	fun IT _ [] = ()
   1.580 -	  | IT n (xtm::xtms) =
   1.581 -	    (Array.update(terms,n,XMLtm xtm);
   1.582 -	     IT (n+1) xtms)
   1.583 -	val _ = IT 0 xtms
   1.584 +        fun IT _ [] = ()
   1.585 +          | IT n (xtm::xtms) =
   1.586 +            (Array.update(terms,n,XMLtm xtm);
   1.587 +             IT (n+1) xtms)
   1.588 +        val _ = IT 0 xtms
   1.589      in
   1.590 -	terms
   1.591 +        terms
   1.592      end
   1.593    | input_terms _ _ _ = raise ERR "input_terms" "Bad term list"
   1.594  end
   1.595  
   1.596  fun get_proof_dir (thyname:string) thy =
   1.597      let
   1.598 -	val import_segment =
   1.599 -	    case get_segment2 thyname thy of
   1.600 -		SOME seg => seg
   1.601 -	      | NONE => get_import_segment thy
   1.602 -	val path = space_explode ":" (getenv "HOL4_PROOFS")
   1.603 -	fun find [] = NONE
   1.604 -	  | find (p::ps) =
   1.605 -	    (let
   1.606 -		 val dir = OS.Path.joinDirFile {dir = p,file=import_segment}
   1.607 -	     in
   1.608 -		 if OS.FileSys.isDir dir
   1.609 -		 then SOME dir
   1.610 -		 else find ps
   1.611 -	     end) handle OS.SysErr _ => find ps
   1.612 +        val import_segment =
   1.613 +            case get_segment2 thyname thy of
   1.614 +                SOME seg => seg
   1.615 +              | NONE => get_import_segment thy
   1.616 +        val path = space_explode ":" (getenv "HOL4_PROOFS")
   1.617 +        fun find [] = NONE
   1.618 +          | find (p::ps) =
   1.619 +            (let
   1.620 +                 val dir = OS.Path.joinDirFile {dir = p,file=import_segment}
   1.621 +             in
   1.622 +                 if OS.FileSys.isDir dir
   1.623 +                 then SOME dir
   1.624 +                 else find ps
   1.625 +             end) handle OS.SysErr _ => find ps
   1.626      in
   1.627 -	Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
   1.628 +        Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
   1.629      end
   1.630  
   1.631  fun proof_file_name thyname thmname thy =
   1.632      let
   1.633 -	val path = case get_proof_dir thyname thy of
   1.634 -		       SOME p => p
   1.635 -		     | NONE => error "Cannot find proof files"
   1.636 -	val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
   1.637 +        val path = case get_proof_dir thyname thy of
   1.638 +                       SOME p => p
   1.639 +                     | NONE => error "Cannot find proof files"
   1.640 +        val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
   1.641      in
   1.642 -	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
   1.643 +        OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
   1.644      end
   1.645  
   1.646  fun xml_to_proof thyname types terms prf thy =
   1.647      let
   1.648 -	val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
   1.649 -	val xml_to_term = TermNet.get_term_from_xml thy thyname types terms
   1.650 +        val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
   1.651 +        val xml_to_term = TermNet.get_term_from_xml thy thyname types terms
   1.652  
   1.653 -	fun index_to_term is =
   1.654 -	    TermNet.get_term_from_index thy thyname types terms is
   1.655 +        fun index_to_term is =
   1.656 +            TermNet.get_term_from_index thy thyname types terms is
   1.657  
   1.658 -	fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is))
   1.659 -	  | x2p (Elem("pinstt",[],p::lambda)) =
   1.660 -	    let
   1.661 -		val p = x2p p
   1.662 -		val lambda = implode_subst (map xml_to_hol_type lambda)
   1.663 -	    in
   1.664 -		mk_proof (PInstT(p,lambda))
   1.665 -	    end
   1.666 -	  | x2p (Elem("psubst",[("i",is)],prf::prfs)) =
   1.667 -	    let
   1.668 -		val tm = index_to_term is
   1.669 -		val prf = x2p prf
   1.670 -		val prfs = map x2p prfs
   1.671 -	    in
   1.672 -		mk_proof (PSubst(prfs,tm,prf))
   1.673 -	    end
   1.674 -	  | x2p (Elem("pabs",[("i",is)],[prf])) =
   1.675 -	    let
   1.676 -		val p = x2p prf
   1.677 -		val t = index_to_term is
   1.678 -	    in
   1.679 -		mk_proof (PAbs (p,t))
   1.680 -	    end
   1.681 -	  | x2p (Elem("pdisch",[("i",is)],[prf])) =
   1.682 -	    let
   1.683 -		val p = x2p prf
   1.684 -		val t = index_to_term is
   1.685 -	    in
   1.686 -		mk_proof (PDisch (p,t))
   1.687 -	    end
   1.688 -	  | x2p (Elem("pmp",[],[prf1,prf2])) =
   1.689 -	    let
   1.690 -		val p1 = x2p prf1
   1.691 -		val p2 = x2p prf2
   1.692 -	    in
   1.693 -		mk_proof (PMp(p1,p2))
   1.694 -	    end
   1.695 -	  | x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is))
   1.696 -	  | x2p (Elem("paxiom",[("n",n),("i",is)],[])) =
   1.697 -	    mk_proof (PAxm(n,index_to_term is))
   1.698 -	  | x2p (Elem("pfact",atts,[])) =
   1.699 -	    let
   1.700 -		val thyname = get_segment thyname atts
   1.701 -		val thmname = protect_factname (get_name atts)
   1.702 -		val p = mk_proof PDisk
   1.703 -		val _  = set_disk_info_of p thyname thmname
   1.704 -	    in
   1.705 -		p
   1.706 -	    end
   1.707 -	  | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =
   1.708 -	    mk_proof (PDef(seg,protect_constname name,index_to_term is))
   1.709 -	  | x2p (Elem("ptmspec",[("s",seg)],p::names)) =
   1.710 -	    let
   1.711 -		val names = map (fn Elem("name",[("n",name)],[]) => name
   1.712 -				  | _ => raise ERR "x2p" "Bad proof (ptmspec)") names
   1.713 -	    in
   1.714 -		mk_proof (PTmSpec(seg,names,x2p p))
   1.715 -	    end
   1.716 -	  | x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) =
   1.717 -	    let
   1.718 -		val P = xml_to_term xP
   1.719 -		val t = xml_to_term xt
   1.720 -	    in
   1.721 -		mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))
   1.722 -	    end
   1.723 -	  | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
   1.724 -	    mk_proof (PTyDef(seg,protect_tyname name,x2p p))
   1.725 -	  | x2p (xml as Elem("poracle",[],chldr)) =
   1.726 -	    let
   1.727 -		val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
   1.728 -		val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
   1.729 -		val (c,asl) = case terms of
   1.730 -				  [] => raise ERR "x2p" "Bad oracle description"
   1.731 -				| (hd::tl) => (hd,tl)
   1.732 -		val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
   1.733 -	    in
   1.734 -		mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
   1.735 -	    end
   1.736 -	  | x2p (Elem("pspec",[("i",is)],[prf])) =
   1.737 -	    let
   1.738 -		val p = x2p prf
   1.739 -		val tm = index_to_term is
   1.740 -	    in
   1.741 -		mk_proof (PSpec(p,tm))
   1.742 -	    end
   1.743 -	  | x2p (Elem("pinst",[],p::theta)) =
   1.744 -	    let
   1.745 -		val p = x2p p
   1.746 -		val theta = implode_subst (map xml_to_term theta)
   1.747 -	    in
   1.748 -		mk_proof (PInst(p,theta))
   1.749 -	    end
   1.750 -	  | x2p (Elem("pgen",[("i",is)],[prf])) =
   1.751 -	    let
   1.752 -		val p = x2p prf
   1.753 -		val tm = index_to_term is
   1.754 -	    in
   1.755 -		mk_proof (PGen(p,tm))
   1.756 -	    end
   1.757 -	  | x2p (Elem("pgenabs",[],prf::tms)) =
   1.758 -	    let
   1.759 -		val p = x2p prf
   1.760 -		val tml = map xml_to_term tms
   1.761 -	    in
   1.762 -		mk_proof (PGenAbs(p,NONE,tml))
   1.763 -	    end
   1.764 -	  | x2p (Elem("pgenabs",[("i",is)],prf::tms)) =
   1.765 -	    let
   1.766 -		val p = x2p prf
   1.767 -		val tml = map xml_to_term tms
   1.768 -	    in
   1.769 -		mk_proof (PGenAbs(p,SOME (index_to_term is),tml))
   1.770 -	    end
   1.771 -	  | x2p (Elem("pimpas",[],[prf1,prf2])) =
   1.772 -	    let
   1.773 -		val p1 = x2p prf1
   1.774 -		val p2 = x2p prf2
   1.775 -	    in
   1.776 -		mk_proof (PImpAS(p1,p2))
   1.777 -	    end
   1.778 -	  | x2p (Elem("psym",[],[prf])) =
   1.779 -	    let
   1.780 -		val p = x2p prf
   1.781 -	    in
   1.782 -		mk_proof (PSym p)
   1.783 -	    end
   1.784 -	  | x2p (Elem("ptrans",[],[prf1,prf2])) =
   1.785 -	    let
   1.786 -		val p1 = x2p prf1
   1.787 -		val p2 = x2p prf2
   1.788 -	    in
   1.789 -		mk_proof (PTrans(p1,p2))
   1.790 -	    end
   1.791 -	  | x2p (Elem("pcomb",[],[prf1,prf2])) =
   1.792 -	    let
   1.793 -		val p1 = x2p prf1
   1.794 -		val p2 = x2p prf2
   1.795 -	    in
   1.796 -		mk_proof (PComb(p1,p2))
   1.797 -	    end
   1.798 -	  | x2p (Elem("peqmp",[],[prf1,prf2])) =
   1.799 -	    let
   1.800 -		val p1 = x2p prf1
   1.801 -		val p2 = x2p prf2
   1.802 -	    in
   1.803 -		mk_proof (PEqMp(p1,p2))
   1.804 -	    end
   1.805 -	  | x2p (Elem("peqimp",[],[prf])) =
   1.806 -	    let
   1.807 -		val p = x2p prf
   1.808 -	    in
   1.809 -		mk_proof (PEqImp p)
   1.810 -	    end
   1.811 -	  | x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) =
   1.812 -	    let
   1.813 -		val p = x2p prf
   1.814 -		val ex = index_to_term ise
   1.815 -		val w = index_to_term isw
   1.816 -	    in
   1.817 -		mk_proof (PExists(p,ex,w))
   1.818 -	    end
   1.819 -	  | x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) =
   1.820 -	    let
   1.821 -		val v  = index_to_term is
   1.822 -		val p1 = x2p prf1
   1.823 -		val p2 = x2p prf2
   1.824 -	    in
   1.825 -		mk_proof (PChoose(v,p1,p2))
   1.826 -	    end
   1.827 -	  | x2p (Elem("pconj",[],[prf1,prf2])) =
   1.828 -	    let
   1.829 -		val p1 = x2p prf1
   1.830 -		val p2 = x2p prf2
   1.831 -	    in
   1.832 -		mk_proof (PConj(p1,p2))
   1.833 -	    end
   1.834 -	  | x2p (Elem("pconjunct1",[],[prf])) =
   1.835 -	    let
   1.836 -		val p = x2p prf
   1.837 -	    in
   1.838 -		mk_proof (PConjunct1 p)
   1.839 -	    end
   1.840 -	  | x2p (Elem("pconjunct2",[],[prf])) =
   1.841 -	    let
   1.842 -		val p = x2p prf
   1.843 -	    in
   1.844 -		mk_proof (PConjunct2 p)
   1.845 -	    end
   1.846 -	  | x2p (Elem("pdisj1",[("i",is)],[prf])) =
   1.847 -	    let
   1.848 -		val p = x2p prf
   1.849 -		val t = index_to_term is
   1.850 -	    in
   1.851 -		mk_proof (PDisj1 (p,t))
   1.852 -	    end
   1.853 -	  | x2p (Elem("pdisj2",[("i",is)],[prf])) =
   1.854 -	    let
   1.855 -		val p = x2p prf
   1.856 -		val t = index_to_term is
   1.857 -	    in
   1.858 -		mk_proof (PDisj2 (p,t))
   1.859 -	    end
   1.860 -	  | x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) =
   1.861 -	    let
   1.862 -		val p1 = x2p prf1
   1.863 -		val p2 = x2p prf2
   1.864 -		val p3 = x2p prf3
   1.865 -	    in
   1.866 -		mk_proof (PDisjCases(p1,p2,p3))
   1.867 -	    end
   1.868 -	  | x2p (Elem("pnoti",[],[prf])) =
   1.869 -	    let
   1.870 -		val p = x2p prf
   1.871 -	    in
   1.872 -		mk_proof (PNotI p)
   1.873 -	    end
   1.874 -	  | x2p (Elem("pnote",[],[prf])) =
   1.875 -	    let
   1.876 -		val p = x2p prf
   1.877 -	    in
   1.878 -		mk_proof (PNotE p)
   1.879 -	    end
   1.880 -	  | x2p (Elem("pcontr",[("i",is)],[prf])) =
   1.881 -	    let
   1.882 -		val p = x2p prf
   1.883 -		val t = index_to_term is
   1.884 -	    in
   1.885 -		mk_proof (PContr (p,t))
   1.886 -	    end
   1.887 -	  | x2p xml = raise ERR "x2p" "Bad proof"
   1.888 +        fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is))
   1.889 +          | x2p (Elem("pinstt",[],p::lambda)) =
   1.890 +            let
   1.891 +                val p = x2p p
   1.892 +                val lambda = implode_subst (map xml_to_hol_type lambda)
   1.893 +            in
   1.894 +                mk_proof (PInstT(p,lambda))
   1.895 +            end
   1.896 +          | x2p (Elem("psubst",[("i",is)],prf::prfs)) =
   1.897 +            let
   1.898 +                val tm = index_to_term is
   1.899 +                val prf = x2p prf
   1.900 +                val prfs = map x2p prfs
   1.901 +            in
   1.902 +                mk_proof (PSubst(prfs,tm,prf))
   1.903 +            end
   1.904 +          | x2p (Elem("pabs",[("i",is)],[prf])) =
   1.905 +            let
   1.906 +                val p = x2p prf
   1.907 +                val t = index_to_term is
   1.908 +            in
   1.909 +                mk_proof (PAbs (p,t))
   1.910 +            end
   1.911 +          | x2p (Elem("pdisch",[("i",is)],[prf])) =
   1.912 +            let
   1.913 +                val p = x2p prf
   1.914 +                val t = index_to_term is
   1.915 +            in
   1.916 +                mk_proof (PDisch (p,t))
   1.917 +            end
   1.918 +          | x2p (Elem("pmp",[],[prf1,prf2])) =
   1.919 +            let
   1.920 +                val p1 = x2p prf1
   1.921 +                val p2 = x2p prf2
   1.922 +            in
   1.923 +                mk_proof (PMp(p1,p2))
   1.924 +            end
   1.925 +          | x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is))
   1.926 +          | x2p (Elem("paxiom",[("n",n),("i",is)],[])) =
   1.927 +            mk_proof (PAxm(n,index_to_term is))
   1.928 +          | x2p (Elem("pfact",atts,[])) =
   1.929 +            let
   1.930 +                val thyname = get_segment thyname atts
   1.931 +                val thmname = protect_factname (get_name atts)
   1.932 +                val p = mk_proof PDisk
   1.933 +                val _  = set_disk_info_of p thyname thmname
   1.934 +            in
   1.935 +                p
   1.936 +            end
   1.937 +          | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =
   1.938 +            mk_proof (PDef(seg,protect_constname name,index_to_term is))
   1.939 +          | x2p (Elem("ptmspec",[("s",seg)],p::names)) =
   1.940 +            let
   1.941 +                val names = map (fn Elem("name",[("n",name)],[]) => name
   1.942 +                                  | _ => raise ERR "x2p" "Bad proof (ptmspec)") names
   1.943 +            in
   1.944 +                mk_proof (PTmSpec(seg,names,x2p p))
   1.945 +            end
   1.946 +          | x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) =
   1.947 +            let
   1.948 +                val P = xml_to_term xP
   1.949 +                val t = xml_to_term xt
   1.950 +            in
   1.951 +                mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))
   1.952 +            end
   1.953 +          | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
   1.954 +            mk_proof (PTyDef(seg,protect_tyname name,x2p p))
   1.955 +          | x2p (xml as Elem("poracle",[],chldr)) =
   1.956 +            let
   1.957 +                val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
   1.958 +                val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
   1.959 +                val (c,asl) = case terms of
   1.960 +                                  [] => raise ERR "x2p" "Bad oracle description"
   1.961 +                                | (hd::tl) => (hd,tl)
   1.962 +                val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
   1.963 +            in
   1.964 +                mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
   1.965 +            end
   1.966 +          | x2p (Elem("pspec",[("i",is)],[prf])) =
   1.967 +            let
   1.968 +                val p = x2p prf
   1.969 +                val tm = index_to_term is
   1.970 +            in
   1.971 +                mk_proof (PSpec(p,tm))
   1.972 +            end
   1.973 +          | x2p (Elem("pinst",[],p::theta)) =
   1.974 +            let
   1.975 +                val p = x2p p
   1.976 +                val theta = implode_subst (map xml_to_term theta)
   1.977 +            in
   1.978 +                mk_proof (PInst(p,theta))
   1.979 +            end
   1.980 +          | x2p (Elem("pgen",[("i",is)],[prf])) =
   1.981 +            let
   1.982 +                val p = x2p prf
   1.983 +                val tm = index_to_term is
   1.984 +            in
   1.985 +                mk_proof (PGen(p,tm))
   1.986 +            end
   1.987 +          | x2p (Elem("pgenabs",[],prf::tms)) =
   1.988 +            let
   1.989 +                val p = x2p prf
   1.990 +                val tml = map xml_to_term tms
   1.991 +            in
   1.992 +                mk_proof (PGenAbs(p,NONE,tml))
   1.993 +            end
   1.994 +          | x2p (Elem("pgenabs",[("i",is)],prf::tms)) =
   1.995 +            let
   1.996 +                val p = x2p prf
   1.997 +                val tml = map xml_to_term tms
   1.998 +            in
   1.999 +                mk_proof (PGenAbs(p,SOME (index_to_term is),tml))
  1.1000 +            end
  1.1001 +          | x2p (Elem("pimpas",[],[prf1,prf2])) =
  1.1002 +            let
  1.1003 +                val p1 = x2p prf1
  1.1004 +                val p2 = x2p prf2
  1.1005 +            in
  1.1006 +                mk_proof (PImpAS(p1,p2))
  1.1007 +            end
  1.1008 +          | x2p (Elem("psym",[],[prf])) =
  1.1009 +            let
  1.1010 +                val p = x2p prf
  1.1011 +            in
  1.1012 +                mk_proof (PSym p)
  1.1013 +            end
  1.1014 +          | x2p (Elem("ptrans",[],[prf1,prf2])) =
  1.1015 +            let
  1.1016 +                val p1 = x2p prf1
  1.1017 +                val p2 = x2p prf2
  1.1018 +            in
  1.1019 +                mk_proof (PTrans(p1,p2))
  1.1020 +            end
  1.1021 +          | x2p (Elem("pcomb",[],[prf1,prf2])) =
  1.1022 +            let
  1.1023 +                val p1 = x2p prf1
  1.1024 +                val p2 = x2p prf2
  1.1025 +            in
  1.1026 +                mk_proof (PComb(p1,p2))
  1.1027 +            end
  1.1028 +          | x2p (Elem("peqmp",[],[prf1,prf2])) =
  1.1029 +            let
  1.1030 +                val p1 = x2p prf1
  1.1031 +                val p2 = x2p prf2
  1.1032 +            in
  1.1033 +                mk_proof (PEqMp(p1,p2))
  1.1034 +            end
  1.1035 +          | x2p (Elem("peqimp",[],[prf])) =
  1.1036 +            let
  1.1037 +                val p = x2p prf
  1.1038 +            in
  1.1039 +                mk_proof (PEqImp p)
  1.1040 +            end
  1.1041 +          | x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) =
  1.1042 +            let
  1.1043 +                val p = x2p prf
  1.1044 +                val ex = index_to_term ise
  1.1045 +                val w = index_to_term isw
  1.1046 +            in
  1.1047 +                mk_proof (PExists(p,ex,w))
  1.1048 +            end
  1.1049 +          | x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) =
  1.1050 +            let
  1.1051 +                val v  = index_to_term is
  1.1052 +                val p1 = x2p prf1
  1.1053 +                val p2 = x2p prf2
  1.1054 +            in
  1.1055 +                mk_proof (PChoose(v,p1,p2))
  1.1056 +            end
  1.1057 +          | x2p (Elem("pconj",[],[prf1,prf2])) =
  1.1058 +            let
  1.1059 +                val p1 = x2p prf1
  1.1060 +                val p2 = x2p prf2
  1.1061 +            in
  1.1062 +                mk_proof (PConj(p1,p2))
  1.1063 +            end
  1.1064 +          | x2p (Elem("pconjunct1",[],[prf])) =
  1.1065 +            let
  1.1066 +                val p = x2p prf
  1.1067 +            in
  1.1068 +                mk_proof (PConjunct1 p)
  1.1069 +            end
  1.1070 +          | x2p (Elem("pconjunct2",[],[prf])) =
  1.1071 +            let
  1.1072 +                val p = x2p prf
  1.1073 +            in
  1.1074 +                mk_proof (PConjunct2 p)
  1.1075 +            end
  1.1076 +          | x2p (Elem("pdisj1",[("i",is)],[prf])) =
  1.1077 +            let
  1.1078 +                val p = x2p prf
  1.1079 +                val t = index_to_term is
  1.1080 +            in
  1.1081 +                mk_proof (PDisj1 (p,t))
  1.1082 +            end
  1.1083 +          | x2p (Elem("pdisj2",[("i",is)],[prf])) =
  1.1084 +            let
  1.1085 +                val p = x2p prf
  1.1086 +                val t = index_to_term is
  1.1087 +            in
  1.1088 +                mk_proof (PDisj2 (p,t))
  1.1089 +            end
  1.1090 +          | x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) =
  1.1091 +            let
  1.1092 +                val p1 = x2p prf1
  1.1093 +                val p2 = x2p prf2
  1.1094 +                val p3 = x2p prf3
  1.1095 +            in
  1.1096 +                mk_proof (PDisjCases(p1,p2,p3))
  1.1097 +            end
  1.1098 +          | x2p (Elem("pnoti",[],[prf])) =
  1.1099 +            let
  1.1100 +                val p = x2p prf
  1.1101 +            in
  1.1102 +                mk_proof (PNotI p)
  1.1103 +            end
  1.1104 +          | x2p (Elem("pnote",[],[prf])) =
  1.1105 +            let
  1.1106 +                val p = x2p prf
  1.1107 +            in
  1.1108 +                mk_proof (PNotE p)
  1.1109 +            end
  1.1110 +          | x2p (Elem("pcontr",[("i",is)],[prf])) =
  1.1111 +            let
  1.1112 +                val p = x2p prf
  1.1113 +                val t = index_to_term is
  1.1114 +            in
  1.1115 +                mk_proof (PContr (p,t))
  1.1116 +            end
  1.1117 +          | x2p xml = raise ERR "x2p" "Bad proof"
  1.1118      in
  1.1119 -	x2p prf
  1.1120 +        x2p prf
  1.1121      end
  1.1122  
  1.1123  fun import_proof_concl thyname thmname thy =
  1.1124      let
  1.1125 -	val is = TextIO.openIn(proof_file_name thyname thmname thy)
  1.1126 -	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
  1.1127 -	val _ = TextIO.closeIn is
  1.1128 +        val is = TextIO.openIn(proof_file_name thyname thmname thy)
  1.1129 +        val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
  1.1130 +        val _ = TextIO.closeIn is
  1.1131      in
  1.1132 -	case proof_xml of
  1.1133 -	    Elem("proof",[],xtypes::xterms::prf::rest) =>
  1.1134 -	    let
  1.1135 -		val types = TypeNet.input_types thyname xtypes
  1.1136 -		val terms = TermNet.input_terms thyname types xterms
  1.1137 +        case proof_xml of
  1.1138 +            Elem("proof",[],xtypes::xterms::prf::rest) =>
  1.1139 +            let
  1.1140 +                val types = TypeNet.input_types thyname xtypes
  1.1141 +                val terms = TermNet.input_terms thyname types xterms
  1.1142                  fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
  1.1143 -	    in
  1.1144 -		case rest of
  1.1145 -		    [] => NONE
  1.1146 -		  | [xtm] => SOME (f xtm)
  1.1147 -		  | _ => raise ERR "import_proof" "Bad argument list"
  1.1148 -	    end
  1.1149 -	  | _ => raise ERR "import_proof" "Bad proof"
  1.1150 +            in
  1.1151 +                case rest of
  1.1152 +                    [] => NONE
  1.1153 +                  | [xtm] => SOME (f xtm)
  1.1154 +                  | _ => raise ERR "import_proof" "Bad argument list"
  1.1155 +            end
  1.1156 +          | _ => raise ERR "import_proof" "Bad proof"
  1.1157      end
  1.1158  
  1.1159  fun import_proof thyname thmname thy =
  1.1160      let
  1.1161 -	val is = TextIO.openIn(proof_file_name thyname thmname thy)
  1.1162 -	val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
  1.1163 -	val _ = TextIO.closeIn is
  1.1164 +        val is = TextIO.openIn(proof_file_name thyname thmname thy)
  1.1165 +        val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
  1.1166 +        val _ = TextIO.closeIn is
  1.1167      in
  1.1168 -	case proof_xml of
  1.1169 -	    Elem("proof",[],xtypes::xterms::prf::rest) =>
  1.1170 -	    let
  1.1171 -		val types = TypeNet.input_types thyname xtypes
  1.1172 -		val terms = TermNet.input_terms thyname types xterms
  1.1173 -	    in
  1.1174 -		(case rest of
  1.1175 -		     [] => NONE
  1.1176 -		   | [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm)
  1.1177 -		   | _ => raise ERR "import_proof" "Bad argument list",
  1.1178 -		 xml_to_proof thyname types terms prf)
  1.1179 -	    end
  1.1180 -	  | _ => raise ERR "import_proof" "Bad proof"
  1.1181 +        case proof_xml of
  1.1182 +            Elem("proof",[],xtypes::xterms::prf::rest) =>
  1.1183 +            let
  1.1184 +                val types = TypeNet.input_types thyname xtypes
  1.1185 +                val terms = TermNet.input_terms thyname types xterms
  1.1186 +            in
  1.1187 +                (case rest of
  1.1188 +                     [] => NONE
  1.1189 +                   | [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm)
  1.1190 +                   | _ => raise ERR "import_proof" "Bad argument list",
  1.1191 +                 xml_to_proof thyname types terms prf)
  1.1192 +            end
  1.1193 +          | _ => raise ERR "import_proof" "Bad proof"
  1.1194      end
  1.1195  
  1.1196  fun uniq_compose m th i st =
  1.1197      let
  1.1198 -	val res = bicompose false (false,th,m) i st
  1.1199 +        val res = bicompose false (false,th,m) i st
  1.1200      in
  1.1201 -	case Seq.pull res of
  1.1202 -	    SOME (th,rest) => (case Seq.pull rest of
  1.1203 -				   SOME _ => raise ERR "uniq_compose" "Not unique!"
  1.1204 -				 | NONE => th)
  1.1205 -	  | NONE => raise ERR "uniq_compose" "No result"
  1.1206 +        case Seq.pull res of
  1.1207 +            SOME (th,rest) => (case Seq.pull rest of
  1.1208 +                                   SOME _ => raise ERR "uniq_compose" "Not unique!"
  1.1209 +                                 | NONE => th)
  1.1210 +          | NONE => raise ERR "uniq_compose" "No result"
  1.1211      end
  1.1212  
  1.1213  val reflexivity_thm = thm "refl"
  1.1214 @@ -1033,10 +1035,10 @@
  1.1215  
  1.1216  fun beta_eta_thm th =
  1.1217      let
  1.1218 -	val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th))  th
  1.1219 -	val th2 = Thm.equal_elim (Thm.eta_conversion       (cprop_of th1)) th1
  1.1220 +        val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th))  th
  1.1221 +        val th2 = Thm.equal_elim (Thm.eta_conversion       (cprop_of th1)) th1
  1.1222      in
  1.1223 -	th2
  1.1224 +        th2
  1.1225      end
  1.1226  
  1.1227  fun implies_elim_all th =
  1.1228 @@ -1049,38 +1051,38 @@
  1.1229  
  1.1230  fun mk_GEN v th sg =
  1.1231      let
  1.1232 -	val c = HOLogic.dest_Trueprop (concl_of th)
  1.1233 -	val cv = cterm_of sg v
  1.1234 -	val lc = Term.lambda v c
  1.1235 -	val clc = Thm.cterm_of sg lc
  1.1236 -	val cvty = ctyp_of_term cv
  1.1237 -	val th1 = implies_elim_all th
  1.1238 -	val th2 = beta_eta_thm (forall_intr cv th1)
  1.1239 -	val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
  1.1240 -	val c = prop_of th3
  1.1241 -	val vname = fst(dest_Free v)
  1.1242 -	val (cold,cnew) = case c of
  1.1243 -			      tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
  1.1244 -			      (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
  1.1245 -			    | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
  1.1246 -			    | _ => raise ERR "mk_GEN" "Unknown conclusion"
  1.1247 -	val th4 = Thm.rename_boundvars cold cnew th3
  1.1248 -	val res = implies_intr_hyps th4
  1.1249 +        val c = HOLogic.dest_Trueprop (concl_of th)
  1.1250 +        val cv = cterm_of sg v
  1.1251 +        val lc = Term.lambda v c
  1.1252 +        val clc = Thm.cterm_of sg lc
  1.1253 +        val cvty = ctyp_of_term cv
  1.1254 +        val th1 = implies_elim_all th
  1.1255 +        val th2 = beta_eta_thm (forall_intr cv th1)
  1.1256 +        val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
  1.1257 +        val c = prop_of th3
  1.1258 +        val vname = fst(dest_Free v)
  1.1259 +        val (cold,cnew) = case c of
  1.1260 +                              tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
  1.1261 +                              (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
  1.1262 +                            | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
  1.1263 +                            | _ => raise ERR "mk_GEN" "Unknown conclusion"
  1.1264 +        val th4 = Thm.rename_boundvars cold cnew th3
  1.1265 +        val res = implies_intr_hyps th4
  1.1266      in
  1.1267 -	res
  1.1268 +        res
  1.1269      end
  1.1270  
  1.1271  val permute_prems = Thm.permute_prems
  1.1272  
  1.1273  fun rearrange sg tm th =
  1.1274      let
  1.1275 -	val tm' = Envir.beta_eta_contract tm
  1.1276 -	fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
  1.1277 -	  | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
  1.1278 -			     then permute_prems n 1 th
  1.1279 -			     else find ps (n+1)
  1.1280 +        val tm' = Envir.beta_eta_contract tm
  1.1281 +        fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
  1.1282 +          | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
  1.1283 +                             then permute_prems n 1 th
  1.1284 +                             else find ps (n+1)
  1.1285      in
  1.1286 -	find (prems_of th) 0
  1.1287 +        find (prems_of th) 0
  1.1288      end
  1.1289  
  1.1290  fun zip (x::xs) (y::ys) = (x,y)::(zip xs ys)
  1.1291 @@ -1093,17 +1095,17 @@
  1.1292  
  1.1293  val collect_vars =
  1.1294      let
  1.1295 -	fun F vars (Bound _) = vars
  1.1296 -	  | F vars (tm as Free _) =
  1.1297 -	    if tm mem vars
  1.1298 -	    then vars
  1.1299 -	    else (tm::vars)
  1.1300 -	  | F vars (Const _) = vars
  1.1301 -	  | F vars (tm1 $ tm2) = F (F vars tm1) tm2
  1.1302 -	  | F vars (Abs(_,_,body)) = F vars body
  1.1303 -	  | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found"
  1.1304 +        fun F vars (Bound _) = vars
  1.1305 +          | F vars (tm as Free _) =
  1.1306 +            if tm mem vars
  1.1307 +            then vars
  1.1308 +            else (tm::vars)
  1.1309 +          | F vars (Const _) = vars
  1.1310 +          | F vars (tm1 $ tm2) = F (F vars tm1) tm2
  1.1311 +          | F vars (Abs(_,_,body)) = F vars body
  1.1312 +          | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found"
  1.1313      in
  1.1314 -	F []
  1.1315 +        F []
  1.1316      end
  1.1317  
  1.1318  (* Code for disambiguating variablenames (wrt. types) *)
  1.1319 @@ -1122,9 +1124,9 @@
  1.1320  fun has_ren (HOLThm _) = false
  1.1321  
  1.1322  fun prinfo {vars,rens} = (writeln "Vars:";
  1.1323 -			  app prin vars;
  1.1324 -			  writeln "Renaming:";
  1.1325 -			  app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens)
  1.1326 +                          app prin vars;
  1.1327 +                          writeln "Renaming:";
  1.1328 +                          app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens)
  1.1329  
  1.1330  fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm)
  1.1331  
  1.1332 @@ -1202,119 +1204,119 @@
  1.1333  
  1.1334  fun get_hol4_thm thyname thmname thy =
  1.1335      case get_hol4_theorem thyname thmname thy of
  1.1336 -	SOME hth => SOME (HOLThm hth)
  1.1337 +        SOME hth => SOME (HOLThm hth)
  1.1338        | NONE =>
  1.1339 -	let
  1.1340 -	    val pending = HOL4Pending.get thy
  1.1341 -	in
  1.1342 -	    case StringPair.lookup pending (thyname,thmname) of
  1.1343 -		SOME hth => SOME (HOLThm hth)
  1.1344 -	      | NONE => NONE
  1.1345 -	end
  1.1346 +        let
  1.1347 +            val pending = HOL4Pending.get thy
  1.1348 +        in
  1.1349 +            case StringPair.lookup pending (thyname,thmname) of
  1.1350 +                SOME hth => SOME (HOLThm hth)
  1.1351 +              | NONE => NONE
  1.1352 +        end
  1.1353  
  1.1354  fun non_trivial_term_consts tm =
  1.1355      List.filter (fn c => not (c = "Trueprop" orelse
  1.1356 -			 c = "All" orelse
  1.1357 -			 c = "op -->" orelse
  1.1358 -			 c = "op &" orelse
  1.1359 -			 c = "op =")) (Term.term_consts tm)
  1.1360 +                         c = "All" orelse
  1.1361 +                         c = "op -->" orelse
  1.1362 +                         c = "op &" orelse
  1.1363 +                         c = "op =")) (Term.term_consts tm)
  1.1364  
  1.1365  fun match_consts t (* th *) =
  1.1366      let
  1.1367 -	fun add_consts (Const (c, _), cs) =
  1.1368 -	    (case c of
  1.1369 -		 "op =" => Library.insert (op =) "==" cs
  1.1370 -	       | "op -->" => Library.insert (op =) "==>" cs
  1.1371 -	       | "All" => cs
  1.1372 -	       | "all" => cs
  1.1373 -	       | "op &" => cs
  1.1374 -	       | "Trueprop" => cs
  1.1375 -	       | _ => Library.insert (op =) c cs)
  1.1376 -	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
  1.1377 -	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
  1.1378 -	  | add_consts (_, cs) = cs
  1.1379 -	val t_consts = add_consts(t,[])
  1.1380 +        fun add_consts (Const (c, _), cs) =
  1.1381 +            (case c of
  1.1382 +                 "op =" => Library.insert (op =) "==" cs
  1.1383 +               | "op -->" => Library.insert (op =) "==>" cs
  1.1384 +               | "All" => cs
  1.1385 +               | "all" => cs
  1.1386 +               | "op &" => cs
  1.1387 +               | "Trueprop" => cs
  1.1388 +               | _ => Library.insert (op =) c cs)
  1.1389 +          | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
  1.1390 +          | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
  1.1391 +          | add_consts (_, cs) = cs
  1.1392 +        val t_consts = add_consts(t,[])
  1.1393      in
  1.1394 -	fn th => eq_set(t_consts,add_consts(prop_of th,[]))
  1.1395 +        fn th => eq_set(t_consts,add_consts(prop_of th,[]))
  1.1396      end
  1.1397  
  1.1398  fun split_name str =
  1.1399      let
  1.1400 -	val sub = Substring.full str
  1.1401 -	val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub)
  1.1402 -	val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
  1.1403 +        val sub = Substring.full str
  1.1404 +        val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub)
  1.1405 +        val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
  1.1406      in
  1.1407 -	if not (idx = "") andalso u = "_"
  1.1408 -	then SOME (newstr,valOf(Int.fromString idx))
  1.1409 -	else NONE
  1.1410 +        if not (idx = "") andalso u = "_"
  1.1411 +        then SOME (newstr,valOf(Int.fromString idx))
  1.1412 +        else NONE
  1.1413      end
  1.1414      handle _ => NONE
  1.1415  
  1.1416  fun rewrite_hol4_term t thy =
  1.1417      let
  1.1418 -	val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
  1.1419 -	val hol4ss = Simplifier.theory_context thy empty_ss
  1.1420 +        val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
  1.1421 +        val hol4ss = Simplifier.theory_context thy empty_ss
  1.1422            setmksimps single addsimps hol4rews1
  1.1423      in
  1.1424 -	Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
  1.1425 +        Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
  1.1426      end
  1.1427  
  1.1428  fun get_isabelle_thm thyname thmname hol4conc thy =
  1.1429      let
  1.1430 -	val (info,hol4conc') = disamb_term hol4conc
  1.1431 -	val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
  1.1432 -	val isaconc =
  1.1433 -	    case concl_of i2h_conc of
  1.1434 -		Const("==",_) $ lhs $ _ => lhs
  1.1435 -	      | _ => error "get_isabelle_thm" "Bad rewrite rule"
  1.1436 -	val _ = (message "Original conclusion:";
  1.1437 -		 if_debug prin hol4conc';
  1.1438 -		 message "Modified conclusion:";
  1.1439 -		 if_debug prin isaconc)
  1.1440 +        val (info,hol4conc') = disamb_term hol4conc
  1.1441 +        val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
  1.1442 +        val isaconc =
  1.1443 +            case concl_of i2h_conc of
  1.1444 +                Const("==",_) $ lhs $ _ => lhs
  1.1445 +              | _ => error "get_isabelle_thm" "Bad rewrite rule"
  1.1446 +        val _ = (message "Original conclusion:";
  1.1447 +                 if_debug prin hol4conc';
  1.1448 +                 message "Modified conclusion:";
  1.1449 +                 if_debug prin isaconc)
  1.1450  
  1.1451 -	fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
  1.1452 +        fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
  1.1453      in
  1.1454 -	case get_hol4_mapping thyname thmname thy of
  1.1455 -	    SOME (SOME thmname) =>
  1.1456 -	    let
  1.1457 -		val th1 = (SOME (PureThy.get_thm thy thmname)
  1.1458 -			   handle ERROR _ =>
  1.1459 -				  (case split_name thmname of
  1.1460 -				       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
  1.1461 -							       handle _ => NONE)
  1.1462 -				     | NONE => NONE))
  1.1463 -	    in
  1.1464 -		case th1 of
  1.1465 -		    SOME th2 =>
  1.1466 -		    (case Shuffler.set_prop thy isaconc [(thmname,th2)] of
  1.1467 -			 SOME (_,th) => (message "YES";(thy, SOME (mk_res th)))
  1.1468 -		       | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping"))
  1.1469 -		  | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping")
  1.1470 -	    end
  1.1471 -	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
  1.1472 -	  | NONE =>
  1.1473 -	    let
  1.1474 -		val _ = (message "Looking for conclusion:";
  1.1475 -			 if_debug prin isaconc)
  1.1476 -		val cs = non_trivial_term_consts isaconc
  1.1477 -		val _ = (message "Looking for consts:";
  1.1478 -			 message (commas cs))
  1.1479 -		val pot_thms = Shuffler.find_potential thy isaconc
  1.1480 -		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
  1.1481 -	    in
  1.1482 -		case Shuffler.set_prop thy isaconc pot_thms of
  1.1483 -		    SOME (isaname,th) =>
  1.1484 -		    let
  1.1485 -			val hth as HOLThm args = mk_res th
  1.1486 -			val thy' =  thy |> add_hol4_theorem thyname thmname args
  1.1487 -					|> add_hol4_mapping thyname thmname isaname
  1.1488 -			val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
  1.1489 -			val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
  1.1490 -		    in
  1.1491 -			(thy',SOME hth)
  1.1492 -		    end
  1.1493 -		  | NONE => (thy,NONE)
  1.1494 -	    end
  1.1495 +        case get_hol4_mapping thyname thmname thy of
  1.1496 +            SOME (SOME thmname) =>
  1.1497 +            let
  1.1498 +                val th1 = (SOME (PureThy.get_thm thy thmname)
  1.1499 +                           handle ERROR _ =>
  1.1500 +                                  (case split_name thmname of
  1.1501 +                                       SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
  1.1502 +                                                               handle _ => NONE)
  1.1503 +                                     | NONE => NONE))
  1.1504 +            in
  1.1505 +                case th1 of
  1.1506 +                    SOME th2 =>
  1.1507 +                    (case Shuffler.set_prop thy isaconc [(thmname,th2)] of
  1.1508 +                         SOME (_,th) => (message "YES";(thy, SOME (mk_res th)))
  1.1509 +                       | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping"))
  1.1510 +                  | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping")
  1.1511 +            end
  1.1512 +          | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
  1.1513 +          | NONE =>
  1.1514 +            let
  1.1515 +                val _ = (message "Looking for conclusion:";
  1.1516 +                         if_debug prin isaconc)
  1.1517 +                val cs = non_trivial_term_consts isaconc
  1.1518 +                val _ = (message "Looking for consts:";
  1.1519 +                         message (commas cs))
  1.1520 +                val pot_thms = Shuffler.find_potential thy isaconc
  1.1521 +                val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
  1.1522 +            in
  1.1523 +                case Shuffler.set_prop thy isaconc pot_thms of
  1.1524 +                    SOME (isaname,th) =>
  1.1525 +                    let
  1.1526 +                        val hth as HOLThm args = mk_res th
  1.1527 +                        val thy' =  thy |> add_hol4_theorem thyname thmname args
  1.1528 +                                        |> add_hol4_mapping thyname thmname isaname
  1.1529 +                        val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
  1.1530 +                        val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
  1.1531 +                    in
  1.1532 +                        (thy',SOME hth)
  1.1533 +                    end
  1.1534 +                  | NONE => (thy,NONE)
  1.1535 +            end
  1.1536      end
  1.1537      handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE))
  1.1538  
  1.1539 @@ -1323,658 +1325,658 @@
  1.1540      val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
  1.1541      fun warn () =
  1.1542          let
  1.1543 -	    val (info,hol4conc') = disamb_term hol4conc
  1.1544 -	    val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
  1.1545 -	in
  1.1546 -	    case concl_of i2h_conc of
  1.1547 -		Const("==",_) $ lhs $ _ =>
  1.1548 -		(warning ("Failed lookup of theorem '"^thmname^"':");
  1.1549 -	         writeln "Original conclusion:";
  1.1550 -		 prin hol4conc';
  1.1551 -		 writeln "Modified conclusion:";
  1.1552 -		 prin lhs)
  1.1553 -	      | _ => ()
  1.1554 -	end
  1.1555 +            val (info,hol4conc') = disamb_term hol4conc
  1.1556 +            val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
  1.1557 +        in
  1.1558 +            case concl_of i2h_conc of
  1.1559 +                Const("==",_) $ lhs $ _ =>
  1.1560 +                (warning ("Failed lookup of theorem '"^thmname^"':");
  1.1561 +                 writeln "Original conclusion:";
  1.1562 +                 prin hol4conc';
  1.1563 +                 writeln "Modified conclusion:";
  1.1564 +                 prin lhs)
  1.1565 +              | _ => ()
  1.1566 +        end
  1.1567    in
  1.1568        case b of
  1.1569 -	  NONE => (warn () handle _ => (); (a,b))
  1.1570 -	| _ => (a, b)
  1.1571 +          NONE => (warn () handle _ => (); (a,b))
  1.1572 +        | _ => (a, b)
  1.1573    end
  1.1574  
  1.1575  fun get_thm thyname thmname thy =
  1.1576      case get_hol4_thm thyname thmname thy of
  1.1577 -	SOME hth => (thy,SOME hth)
  1.1578 +        SOME hth => (thy,SOME hth)
  1.1579        | NONE => ((case import_proof_concl thyname thmname thy of
  1.1580 -		      SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
  1.1581 -		    | NONE => (message "No conclusion"; (thy,NONE)))
  1.1582 -		 handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
  1.1583 -		      | e as PK _ => (message "PK exception"; (thy,NONE)))
  1.1584 +                      SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
  1.1585 +                    | NONE => (message "No conclusion"; (thy,NONE)))
  1.1586 +                 handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
  1.1587 +                      | e as PK _ => (message "PK exception"; (thy,NONE)))
  1.1588  
  1.1589  fun rename_const thyname thy name =
  1.1590      case get_hol4_const_renaming thyname name thy of
  1.1591 -	SOME cname => cname
  1.1592 +        SOME cname => cname
  1.1593        | NONE => name
  1.1594  
  1.1595  fun get_def thyname constname rhs thy =
  1.1596      let
  1.1597 -	val constname = rename_const thyname thy constname
  1.1598 -	val (thmname,thy') = get_defname thyname constname thy
  1.1599 -	val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname)
  1.1600 +        val constname = rename_const thyname thy constname
  1.1601 +        val (thmname,thy') = get_defname thyname constname thy
  1.1602 +        val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname)
  1.1603      in
  1.1604 -	get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy'
  1.1605 +        get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy'
  1.1606      end
  1.1607  
  1.1608  fun get_axiom thyname axname thy =
  1.1609      case get_thm thyname axname thy of
  1.1610 -	arg as (_,SOME _) => arg
  1.1611 +        arg as (_,SOME _) => arg
  1.1612        | _ => raise ERR "get_axiom" ("Trying to retrieve axiom (" ^ axname ^ ")")
  1.1613  
  1.1614  fun intern_store_thm gen_output thyname thmname hth thy =
  1.1615      let
  1.1616 -	val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
  1.1617 -	val rew = rewrite_hol4_term (concl_of th) thy
  1.1618 -	val th  = equal_elim rew th
  1.1619 -	val thy' = add_hol4_pending thyname thmname args thy
  1.1620 -	val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
  1.1621 +        val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
  1.1622 +        val rew = rewrite_hol4_term (concl_of th) thy
  1.1623 +        val th  = equal_elim rew th
  1.1624 +        val thy' = add_hol4_pending thyname thmname args thy
  1.1625 +        val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
  1.1626          val th = disambiguate_frees th
  1.1627 -	val thy2 = if gen_output
  1.1628 -		   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
  1.1629 +        val thy2 = if gen_output
  1.1630 +                   then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
  1.1631                                    (smart_string_of_thm th) ^ "\n  by (import " ^
  1.1632                                    thyname ^ " " ^ (quotename thmname) ^ ")") thy'
  1.1633 -		   else thy'
  1.1634 +                   else thy'
  1.1635      in
  1.1636 -	(thy2,hth')
  1.1637 +        (thy2,hth')
  1.1638      end
  1.1639  
  1.1640  val store_thm = intern_store_thm true
  1.1641  
  1.1642  fun mk_REFL ctm =
  1.1643      let
  1.1644 -	val cty = Thm.ctyp_of_term ctm
  1.1645 +        val cty = Thm.ctyp_of_term ctm
  1.1646      in
  1.1647 -	Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm
  1.1648 +        Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm
  1.1649      end
  1.1650  
  1.1651  fun REFL tm thy =
  1.1652      let
  1.1653 -	val _ = message "REFL:"
  1.1654 -	val (info,tm') = disamb_term tm
  1.1655 -	val ctm = Thm.cterm_of thy tm'
  1.1656 -	val res = HOLThm(rens_of info,mk_REFL ctm)
  1.1657 -	val _ = if_debug pth res
  1.1658 +        val _ = message "REFL:"
  1.1659 +        val (info,tm') = disamb_term tm
  1.1660 +        val ctm = Thm.cterm_of thy tm'
  1.1661 +        val res = HOLThm(rens_of info,mk_REFL ctm)
  1.1662 +        val _ = if_debug pth res
  1.1663      in
  1.1664 -	(thy,res)
  1.1665 +        (thy,res)
  1.1666      end
  1.1667  
  1.1668  fun ASSUME tm thy =
  1.1669      let
  1.1670 -	val _ = message "ASSUME:"
  1.1671 -	val (info,tm') = disamb_term tm
  1.1672 -	val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm')
  1.1673 -	val th = Thm.trivial ctm
  1.1674 -	val res = HOLThm(rens_of info,th)
  1.1675 -	val _ = if_debug pth res
  1.1676 +        val _ = message "ASSUME:"
  1.1677 +        val (info,tm') = disamb_term tm
  1.1678 +        val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm')
  1.1679 +        val th = Thm.trivial ctm
  1.1680 +        val res = HOLThm(rens_of info,th)
  1.1681 +        val _ = if_debug pth res
  1.1682      in
  1.1683 -	(thy,res)
  1.1684 +        (thy,res)
  1.1685      end
  1.1686  
  1.1687  fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy =
  1.1688      let
  1.1689 -	val _ = message "INST_TYPE:"
  1.1690 -	val _ = if_debug pth hth
  1.1691 -	val tys_before = add_term_tfrees (prop_of th,[])
  1.1692 -	val th1 = Thm.varifyT th
  1.1693 -	val tys_after = add_term_tvars (prop_of th1,[])
  1.1694 -	val tyinst = map (fn (bef, iS) =>
  1.1695 -			     (case try (Lib.assoc (TFree bef)) lambda of
  1.1696 -				  SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
  1.1697 -				| NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
  1.1698 -			     ))
  1.1699 -			 (zip tys_before tys_after)
  1.1700 -	val res = Drule.instantiate (tyinst,[]) th1
  1.1701 -	val hth = HOLThm([],res)
  1.1702 -	val res = norm_hthm thy hth
  1.1703 -	val _ = message "RESULT:"
  1.1704 -	val _ = if_debug pth res
  1.1705 +        val _ = message "INST_TYPE:"
  1.1706 +        val _ = if_debug pth hth
  1.1707 +        val tys_before = add_term_tfrees (prop_of th,[])
  1.1708 +        val th1 = Thm.varifyT th
  1.1709 +        val tys_after = add_term_tvars (prop_of th1,[])
  1.1710 +        val tyinst = map (fn (bef, iS) =>
  1.1711 +                             (case try (Lib.assoc (TFree bef)) lambda of
  1.1712 +                                  SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
  1.1713 +                                | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
  1.1714 +                             ))
  1.1715 +                         (zip tys_before tys_after)
  1.1716 +        val res = Drule.instantiate (tyinst,[]) th1
  1.1717 +        val hth = HOLThm([],res)
  1.1718 +        val res = norm_hthm thy hth
  1.1719 +        val _ = message "RESULT:"
  1.1720 +        val _ = if_debug pth res
  1.1721      in
  1.1722 -	(thy,res)
  1.1723 +        (thy,res)
  1.1724      end
  1.1725  
  1.1726  fun INST sigma hth thy =
  1.1727      let
  1.1728 -	val _ = message "INST:"
  1.1729 -	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
  1.1730 -	val _ = if_debug pth hth
  1.1731 -	val (sdom,srng) = ListPair.unzip (rev sigma)
  1.1732 -	val th = hthm2thm hth
  1.1733 -	val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th
  1.1734 -	val res = HOLThm([],th1)
  1.1735 -	val _ = message "RESULT:"
  1.1736 -	val _ = if_debug pth res
  1.1737 +        val _ = message "INST:"
  1.1738 +        val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
  1.1739 +        val _ = if_debug pth hth
  1.1740 +        val (sdom,srng) = ListPair.unzip (rev sigma)
  1.1741 +        val th = hthm2thm hth
  1.1742 +        val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th
  1.1743 +        val res = HOLThm([],th1)
  1.1744 +        val _ = message "RESULT:"
  1.1745 +        val _ = if_debug pth res
  1.1746      in
  1.1747 -	(thy,res)
  1.1748 +        (thy,res)
  1.1749      end
  1.1750  
  1.1751  fun EQ_IMP_RULE (hth as HOLThm(rens,th)) thy =
  1.1752      let
  1.1753 -	val _ = message "EQ_IMP_RULE:"
  1.1754 -	val _ = if_debug pth hth
  1.1755 -	val res = HOLThm(rens,th RS eqimp_thm)
  1.1756 -	val _ = message "RESULT:"
  1.1757 -	val _ = if_debug pth res
  1.1758 +        val _ = message "EQ_IMP_RULE:"
  1.1759 +        val _ = if_debug pth hth
  1.1760 +        val res = HOLThm(rens,th RS eqimp_thm)
  1.1761 +        val _ = message "RESULT:"
  1.1762 +        val _ = if_debug pth res
  1.1763      in
  1.1764 -	(thy,res)
  1.1765 +        (thy,res)
  1.1766      end
  1.1767  
  1.1768  fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm
  1.1769  
  1.1770  fun EQ_MP hth1 hth2 thy =
  1.1771      let
  1.1772 -	val _ = message "EQ_MP:"
  1.1773 -	val _ = if_debug pth hth1
  1.1774 -	val _ = if_debug pth hth2
  1.1775 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.1776 -	val res = HOLThm(rens_of info,mk_EQ_MP th1 th2)
  1.1777 -	val _ = message "RESULT:"
  1.1778 -	val _ = if_debug pth res
  1.1779 +        val _ = message "EQ_MP:"
  1.1780 +        val _ = if_debug pth hth1
  1.1781 +        val _ = if_debug pth hth2
  1.1782 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.1783 +        val res = HOLThm(rens_of info,mk_EQ_MP th1 th2)
  1.1784 +        val _ = message "RESULT:"
  1.1785 +        val _ = if_debug pth res
  1.1786      in
  1.1787 -	(thy,res)
  1.1788 +        (thy,res)
  1.1789      end
  1.1790  
  1.1791  fun mk_COMB th1 th2 thy =
  1.1792      let
  1.1793 -	val (f,g) = case concl_of th1 of
  1.1794 -			_ $ (Const("op =",_) $ f $ g) => (f,g)
  1.1795 -		      | _ => raise ERR "mk_COMB" "First theorem not an equality"
  1.1796 -	val (x,y) = case concl_of th2 of
  1.1797 -			_ $ (Const("op =",_) $ x $ y) => (x,y)
  1.1798 -		      | _ => raise ERR "mk_COMB" "Second theorem not an equality"
  1.1799 -	val fty = type_of f
  1.1800 -	val (fd,fr) = dom_rng fty
  1.1801 -	val comb_thm' = Drule.instantiate'
  1.1802 -			    [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
  1.1803 -			    [SOME (cterm_of thy f),SOME (cterm_of thy g),
  1.1804 -			     SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm
  1.1805 +        val (f,g) = case concl_of th1 of
  1.1806 +                        _ $ (Const("op =",_) $ f $ g) => (f,g)
  1.1807 +                      | _ => raise ERR "mk_COMB" "First theorem not an equality"
  1.1808 +        val (x,y) = case concl_of th2 of
  1.1809 +                        _ $ (Const("op =",_) $ x $ y) => (x,y)
  1.1810 +                      | _ => raise ERR "mk_COMB" "Second theorem not an equality"
  1.1811 +        val fty = type_of f
  1.1812 +        val (fd,fr) = dom_rng fty
  1.1813 +        val comb_thm' = Drule.instantiate'
  1.1814 +                            [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
  1.1815 +                            [SOME (cterm_of thy f),SOME (cterm_of thy g),
  1.1816 +                             SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm
  1.1817      in
  1.1818 -	[th1,th2] MRS comb_thm'
  1.1819 +        [th1,th2] MRS comb_thm'
  1.1820      end
  1.1821  
  1.1822  fun SUBST rews ctxt hth thy =
  1.1823      let
  1.1824 -	val _ = message "SUBST:"
  1.1825 -	val _ = if_debug (app pth) rews
  1.1826 -	val _ = if_debug prin ctxt
  1.1827 -	val _ = if_debug pth hth
  1.1828 -	val (info,th) = disamb_thm hth
  1.1829 -	val (info1,ctxt') = disamb_term_from info ctxt
  1.1830 -	val (info2,rews') = disamb_thms_from info1 rews
  1.1831 +        val _ = message "SUBST:"
  1.1832 +        val _ = if_debug (app pth) rews
  1.1833 +        val _ = if_debug prin ctxt
  1.1834 +        val _ = if_debug pth hth
  1.1835 +        val (info,th) = disamb_thm hth
  1.1836 +        val (info1,ctxt') = disamb_term_from info ctxt
  1.1837 +        val (info2,rews') = disamb_thms_from info1 rews
  1.1838  
  1.1839 -	val cctxt = cterm_of thy ctxt'
  1.1840 -	fun subst th [] = th
  1.1841 -	  | subst th (rew::rews) = subst (mk_COMB th rew thy) rews
  1.1842 -	val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th)
  1.1843 -	val _ = message "RESULT:"
  1.1844 -	val _ = if_debug pth res
  1.1845 +        val cctxt = cterm_of thy ctxt'
  1.1846 +        fun subst th [] = th
  1.1847 +          | subst th (rew::rews) = subst (mk_COMB th rew thy) rews
  1.1848 +        val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th)
  1.1849 +        val _ = message "RESULT:"
  1.1850 +        val _ = if_debug pth res
  1.1851      in
  1.1852 -	(thy,res)
  1.1853 +        (thy,res)
  1.1854      end
  1.1855  
  1.1856  fun DISJ_CASES hth hth1 hth2 thy =
  1.1857      let
  1.1858 -	val _ = message "DISJ_CASES:"
  1.1859 -	val _ = if_debug (app pth) [hth,hth1,hth2]
  1.1860 -	val (info,th) = disamb_thm hth
  1.1861 -	val (info1,th1) = disamb_thm_from info hth1
  1.1862 -	val (info2,th2) = disamb_thm_from info1 hth2
  1.1863 -	val th1 = norm_hyps th1
  1.1864 -	val th2 = norm_hyps th2
  1.1865 -	val (l,r) = case concl_of th of
  1.1866 -			_ $ (Const("op |",_) $ l $ r) => (l,r)
  1.1867 -		      | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
  1.1868 -	val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
  1.1869 -	val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
  1.1870 -	val res1 = th RS disj_cases_thm
  1.1871 -	val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1
  1.1872 -	val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2
  1.1873 -	val res  = HOLThm(rens_of info2,res3)
  1.1874 -	val _ = message "RESULT:"
  1.1875 -	val _ = if_debug pth res
  1.1876 +        val _ = message "DISJ_CASES:"
  1.1877 +        val _ = if_debug (app pth) [hth,hth1,hth2]
  1.1878 +        val (info,th) = disamb_thm hth
  1.1879 +        val (info1,th1) = disamb_thm_from info hth1
  1.1880 +        val (info2,th2) = disamb_thm_from info1 hth2
  1.1881 +        val th1 = norm_hyps th1
  1.1882 +        val th2 = norm_hyps th2
  1.1883 +        val (l,r) = case concl_of th of
  1.1884 +                        _ $ (Const("op |",_) $ l $ r) => (l,r)
  1.1885 +                      | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
  1.1886 +        val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
  1.1887 +        val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
  1.1888 +        val res1 = th RS disj_cases_thm
  1.1889 +        val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1
  1.1890 +        val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2
  1.1891 +        val res  = HOLThm(rens_of info2,res3)
  1.1892 +        val _ = message "RESULT:"
  1.1893 +        val _ = if_debug pth res
  1.1894      in
  1.1895 -	(thy,res)
  1.1896 +        (thy,res)
  1.1897      end
  1.1898  
  1.1899  fun DISJ1 hth tm thy =
  1.1900      let
  1.1901 -	val _ = message "DISJ1:"
  1.1902 -	val _ = if_debug pth hth
  1.1903 -	val _ = if_debug prin tm
  1.1904 -	val (info,th) = disamb_thm hth
  1.1905 -	val (info',tm') = disamb_term_from info tm
  1.1906 -	val ct = Thm.cterm_of thy tm'
  1.1907 -	val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm
  1.1908 -	val res = HOLThm(rens_of info',th RS disj1_thm')
  1.1909 -	val _ = message "RESULT:"
  1.1910 -	val _ = if_debug pth res
  1.1911 +        val _ = message "DISJ1:"
  1.1912 +        val _ = if_debug pth hth
  1.1913 +        val _ = if_debug prin tm
  1.1914 +        val (info,th) = disamb_thm hth
  1.1915 +        val (info',tm') = disamb_term_from info tm
  1.1916 +        val ct = Thm.cterm_of thy tm'
  1.1917 +        val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm
  1.1918 +        val res = HOLThm(rens_of info',th RS disj1_thm')
  1.1919 +        val _ = message "RESULT:"
  1.1920 +        val _ = if_debug pth res
  1.1921      in
  1.1922 -	(thy,res)
  1.1923 +        (thy,res)
  1.1924      end
  1.1925  
  1.1926  fun DISJ2 tm hth thy =
  1.1927      let
  1.1928 -	val _ = message "DISJ1:"
  1.1929 -	val _ = if_debug prin tm
  1.1930 -	val _ = if_debug pth hth
  1.1931 -	val (info,th) = disamb_thm hth
  1.1932 -	val (info',tm') = disamb_term_from info tm
  1.1933 -	val ct = Thm.cterm_of thy tm'
  1.1934 -	val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm
  1.1935 -	val res = HOLThm(rens_of info',th RS disj2_thm')
  1.1936 -	val _ = message "RESULT:"
  1.1937 -	val _ = if_debug pth res
  1.1938 +        val _ = message "DISJ1:"
  1.1939 +        val _ = if_debug prin tm
  1.1940 +        val _ = if_debug pth hth
  1.1941 +        val (info,th) = disamb_thm hth
  1.1942 +        val (info',tm') = disamb_term_from info tm
  1.1943 +        val ct = Thm.cterm_of thy tm'
  1.1944 +        val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm
  1.1945 +        val res = HOLThm(rens_of info',th RS disj2_thm')
  1.1946 +        val _ = message "RESULT:"
  1.1947 +        val _ = if_debug pth res
  1.1948      in
  1.1949 -	(thy,res)
  1.1950 +        (thy,res)
  1.1951      end
  1.1952  
  1.1953  fun IMP_ANTISYM hth1 hth2 thy =
  1.1954      let
  1.1955 -	val _ = message "IMP_ANTISYM:"
  1.1956 -	val _ = if_debug pth hth1
  1.1957 -	val _ = if_debug pth hth2
  1.1958 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.1959 -	val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm
  1.1960 -	val res = HOLThm(rens_of info,th)
  1.1961 -	val _ = message "RESULT:"
  1.1962 -	val _ = if_debug pth res
  1.1963 +        val _ = message "IMP_ANTISYM:"
  1.1964 +        val _ = if_debug pth hth1
  1.1965 +        val _ = if_debug pth hth2
  1.1966 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.1967 +        val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm
  1.1968 +        val res = HOLThm(rens_of info,th)
  1.1969 +        val _ = message "RESULT:"
  1.1970 +        val _ = if_debug pth res
  1.1971      in
  1.1972 -	(thy,res)
  1.1973 +        (thy,res)
  1.1974      end
  1.1975  
  1.1976  fun SYM (hth as HOLThm(rens,th)) thy =
  1.1977      let
  1.1978 -	val _ = message "SYM:"
  1.1979 -	val _ = if_debug pth hth
  1.1980 -	val th = th RS symmetry_thm
  1.1981 -	val res = HOLThm(rens,th)
  1.1982 -	val _ = message "RESULT:"
  1.1983 -	val _ = if_debug pth res
  1.1984 +        val _ = message "SYM:"
  1.1985 +        val _ = if_debug pth hth
  1.1986 +        val th = th RS symmetry_thm
  1.1987 +        val res = HOLThm(rens,th)
  1.1988 +        val _ = message "RESULT:"
  1.1989 +        val _ = if_debug pth res
  1.1990      in
  1.1991 -	(thy,res)
  1.1992 +        (thy,res)
  1.1993      end
  1.1994  
  1.1995  fun MP hth1 hth2 thy =
  1.1996      let
  1.1997 -	val _ = message "MP:"
  1.1998 -	val _ = if_debug pth hth1
  1.1999 -	val _ = if_debug pth hth2
  1.2000 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2001 -	val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm
  1.2002 -	val res = HOLThm(rens_of info,th)
  1.2003 -	val _ = message "RESULT:"
  1.2004 -	val _ = if_debug pth res
  1.2005 +        val _ = message "MP:"
  1.2006 +        val _ = if_debug pth hth1
  1.2007 +        val _ = if_debug pth hth2
  1.2008 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2009 +        val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm
  1.2010 +        val res = HOLThm(rens_of info,th)
  1.2011 +        val _ = message "RESULT:"
  1.2012 +        val _ = if_debug pth res
  1.2013      in
  1.2014 -	(thy,res)
  1.2015 +        (thy,res)
  1.2016      end
  1.2017  
  1.2018  fun CONJ hth1 hth2 thy =
  1.2019      let
  1.2020 -	val _ = message "CONJ:"
  1.2021 -	val _ = if_debug pth hth1
  1.2022 -	val _ = if_debug pth hth2
  1.2023 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2024 -	val th = [th1,th2] MRS conj_thm
  1.2025 -	val res = HOLThm(rens_of info,th)
  1.2026 -	val _ = message "RESULT:"
  1.2027 -	val _ = if_debug pth res
  1.2028 +        val _ = message "CONJ:"
  1.2029 +        val _ = if_debug pth hth1
  1.2030 +        val _ = if_debug pth hth2
  1.2031 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2032 +        val th = [th1,th2] MRS conj_thm
  1.2033 +        val res = HOLThm(rens_of info,th)
  1.2034 +        val _ = message "RESULT:"
  1.2035 +        val _ = if_debug pth res
  1.2036      in
  1.2037 -	(thy,res)
  1.2038 +        (thy,res)
  1.2039      end
  1.2040  
  1.2041  fun CONJUNCT1 (hth as HOLThm(rens,th)) thy =
  1.2042      let
  1.2043 -	val _ = message "CONJUNCT1:"
  1.2044 -	val _ = if_debug pth hth
  1.2045 -	val res = HOLThm(rens,th RS conjunct1_thm)
  1.2046 -	val _ = message "RESULT:"
  1.2047 -	val _ = if_debug pth res
  1.2048 +        val _ = message "CONJUNCT1:"
  1.2049 +        val _ = if_debug pth hth
  1.2050 +        val res = HOLThm(rens,th RS conjunct1_thm)
  1.2051 +        val _ = message "RESULT:"
  1.2052 +        val _ = if_debug pth res
  1.2053      in
  1.2054 -	(thy,res)
  1.2055 +        (thy,res)
  1.2056      end
  1.2057  
  1.2058  fun CONJUNCT2 (hth as HOLThm(rens,th)) thy =
  1.2059      let
  1.2060 -	val _ = message "CONJUNCT1:"
  1.2061 -	val _ = if_debug pth hth
  1.2062 -	val res = HOLThm(rens,th RS conjunct2_thm)
  1.2063 -	val _ = message "RESULT:"
  1.2064 -	val _ = if_debug pth res
  1.2065 +        val _ = message "CONJUNCT1:"
  1.2066 +        val _ = if_debug pth hth
  1.2067 +        val res = HOLThm(rens,th RS conjunct2_thm)
  1.2068 +        val _ = message "RESULT:"
  1.2069 +        val _ = if_debug pth res
  1.2070      in
  1.2071 -	(thy,res)
  1.2072 +        (thy,res)
  1.2073      end
  1.2074  
  1.2075  fun EXISTS ex wit hth thy =
  1.2076      let
  1.2077 -	val _ = message "EXISTS:"
  1.2078 -	val _ = if_debug prin ex
  1.2079 -	val _ = if_debug prin wit
  1.2080 -	val _ = if_debug pth hth
  1.2081 -	val (info,th) = disamb_thm hth
  1.2082 -	val (info',[ex',wit']) = disamb_terms_from info [ex,wit]
  1.2083 -	val cwit = cterm_of thy wit'
  1.2084 -	val cty = ctyp_of_term cwit
  1.2085 -	val a = case ex' of
  1.2086 -		    (Const("Ex",_) $ a) => a
  1.2087 -		  | _ => raise ERR "EXISTS" "Argument not existential"
  1.2088 -	val ca = cterm_of thy a
  1.2089 -	val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
  1.2090 -	val th1 = beta_eta_thm th
  1.2091 -	val th2 = implies_elim_all th1
  1.2092 -	val th3 = th2 COMP exists_thm'
  1.2093 -	val th  = implies_intr_hyps th3
  1.2094 -	val res = HOLThm(rens_of info',th)
  1.2095 -	val _   = message "RESULT:"
  1.2096 -	val _   = if_debug pth res
  1.2097 +        val _ = message "EXISTS:"
  1.2098 +        val _ = if_debug prin ex
  1.2099 +        val _ = if_debug prin wit
  1.2100 +        val _ = if_debug pth hth
  1.2101 +        val (info,th) = disamb_thm hth
  1.2102 +        val (info',[ex',wit']) = disamb_terms_from info [ex,wit]
  1.2103 +        val cwit = cterm_of thy wit'
  1.2104 +        val cty = ctyp_of_term cwit
  1.2105 +        val a = case ex' of
  1.2106 +                    (Const("Ex",_) $ a) => a
  1.2107 +                  | _ => raise ERR "EXISTS" "Argument not existential"
  1.2108 +        val ca = cterm_of thy a
  1.2109 +        val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
  1.2110 +        val th1 = beta_eta_thm th
  1.2111 +        val th2 = implies_elim_all th1
  1.2112 +        val th3 = th2 COMP exists_thm'
  1.2113 +        val th  = implies_intr_hyps th3
  1.2114 +        val res = HOLThm(rens_of info',th)
  1.2115 +        val _   = message "RESULT:"
  1.2116 +        val _   = if_debug pth res
  1.2117      in
  1.2118 -	(thy,res)
  1.2119 +        (thy,res)
  1.2120      end
  1.2121  
  1.2122  fun CHOOSE v hth1 hth2 thy =
  1.2123      let
  1.2124 -	val _ = message "CHOOSE:"
  1.2125 -	val _ = if_debug prin v
  1.2126 -	val _ = if_debug pth hth1
  1.2127 -	val _ = if_debug pth hth2
  1.2128 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2129 -	val (info',v') = disamb_term_from info v
  1.2130 -	fun strip 0 _ th = th
  1.2131 -	  | strip n (p::ps) th =
  1.2132 -	    strip (n-1) ps (implies_elim th (assume p))
  1.2133 -	  | strip _ _ _ = raise ERR "CHOOSE" "strip error"
  1.2134 -	val cv = cterm_of thy v'
  1.2135 -	val th2 = norm_hyps th2
  1.2136 -	val cvty = ctyp_of_term cv
  1.2137 -	val c = HOLogic.dest_Trueprop (concl_of th2)
  1.2138 -	val cc = cterm_of thy c
  1.2139 -	val a = case concl_of th1 of
  1.2140 -		    _ $ (Const("Ex",_) $ a) => a
  1.2141 -		  | _ => raise ERR "CHOOSE" "Conclusion not existential"
  1.2142 -	val ca = cterm_of (theory_of_thm th1) a
  1.2143 -	val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
  1.2144 -	val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
  1.2145 -	val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
  1.2146 -	val th23 = beta_eta_thm (forall_intr cv th22)
  1.2147 -	val th11 = implies_elim_all (beta_eta_thm th1)
  1.2148 -	val th' = th23 COMP (th11 COMP choose_thm')
  1.2149 -	val th = implies_intr_hyps th'
  1.2150 -	val res = HOLThm(rens_of info',th)
  1.2151 -	val _   = message "RESULT:"
  1.2152 -	val _   = if_debug pth res
  1.2153 +        val _ = message "CHOOSE:"
  1.2154 +        val _ = if_debug prin v
  1.2155 +        val _ = if_debug pth hth1
  1.2156 +        val _ = if_debug pth hth2
  1.2157 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2158 +        val (info',v') = disamb_term_from info v
  1.2159 +        fun strip 0 _ th = th
  1.2160 +          | strip n (p::ps) th =
  1.2161 +            strip (n-1) ps (implies_elim th (assume p))
  1.2162 +          | strip _ _ _ = raise ERR "CHOOSE" "strip error"
  1.2163 +        val cv = cterm_of thy v'
  1.2164 +        val th2 = norm_hyps th2
  1.2165 +        val cvty = ctyp_of_term cv
  1.2166 +        val c = HOLogic.dest_Trueprop (concl_of th2)
  1.2167 +        val cc = cterm_of thy c
  1.2168 +        val a = case concl_of th1 of
  1.2169 +                    _ $ (Const("Ex",_) $ a) => a
  1.2170 +                  | _ => raise ERR "CHOOSE" "Conclusion not existential"
  1.2171 +        val ca = cterm_of (theory_of_thm th1) a
  1.2172 +        val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
  1.2173 +        val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
  1.2174 +        val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
  1.2175 +        val th23 = beta_eta_thm (forall_intr cv th22)
  1.2176 +        val th11 = implies_elim_all (beta_eta_thm th1)
  1.2177 +        val th' = th23 COMP (th11 COMP choose_thm')
  1.2178 +        val th = implies_intr_hyps th'
  1.2179 +        val res = HOLThm(rens_of info',th)
  1.2180 +        val _   = message "RESULT:"
  1.2181 +        val _   = if_debug pth res
  1.2182      in
  1.2183 -	(thy,res)
  1.2184 +        (thy,res)
  1.2185      end
  1.2186  
  1.2187  fun GEN v hth thy =
  1.2188      let
  1.2189        val _ = message "GEN:"
  1.2190 -	val _ = if_debug prin v
  1.2191 -	val _ = if_debug pth hth
  1.2192 -	val (info,th) = disamb_thm hth
  1.2193 -	val (info',v') = disamb_term_from info v
  1.2194 -	val res = HOLThm(rens_of info',mk_GEN v' th thy)
  1.2195 -	val _ = message "RESULT:"
  1.2196 -	val _ = if_debug pth res
  1.2197 +        val _ = if_debug prin v
  1.2198 +        val _ = if_debug pth hth
  1.2199 +        val (info,th) = disamb_thm hth
  1.2200 +        val (info',v') = disamb_term_from info v
  1.2201 +        val res = HOLThm(rens_of info',mk_GEN v' th thy)
  1.2202 +        val _ = message "RESULT:"
  1.2203 +        val _ = if_debug pth res
  1.2204      in
  1.2205 -	(thy,res)
  1.2206 +        (thy,res)
  1.2207      end
  1.2208  
  1.2209  fun SPEC tm hth thy =
  1.2210      let
  1.2211 -	val _ = message "SPEC:"
  1.2212 -	val _ = if_debug prin tm
  1.2213 -	val _ = if_debug pth hth
  1.2214 -	val (info,th) = disamb_thm hth
  1.2215 -	val (info',tm') = disamb_term_from info tm
  1.2216 -	val ctm = Thm.cterm_of thy tm'
  1.2217 -	val cty = Thm.ctyp_of_term ctm
  1.2218 -	val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm
  1.2219 -	val th = th RS spec'
  1.2220 -	val res = HOLThm(rens_of info',th)
  1.2221 -	val _ = message "RESULT:"
  1.2222 -	val _ = if_debug pth res
  1.2223 +        val _ = message "SPEC:"
  1.2224 +        val _ = if_debug prin tm
  1.2225 +        val _ = if_debug pth hth
  1.2226 +        val (info,th) = disamb_thm hth
  1.2227 +        val (info',tm') = disamb_term_from info tm
  1.2228 +        val ctm = Thm.cterm_of thy tm'
  1.2229 +        val cty = Thm.ctyp_of_term ctm
  1.2230 +        val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm
  1.2231 +        val th = th RS spec'
  1.2232 +        val res = HOLThm(rens_of info',th)
  1.2233 +        val _ = message "RESULT:"
  1.2234 +        val _ = if_debug pth res
  1.2235      in
  1.2236 -	(thy,res)
  1.2237 +        (thy,res)
  1.2238      end
  1.2239  
  1.2240  fun COMB hth1 hth2 thy =
  1.2241      let
  1.2242 -	val _ = message "COMB:"
  1.2243 -	val _ = if_debug pth hth1
  1.2244 -	val _ = if_debug pth hth2
  1.2245 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2246 -	val res = HOLThm(rens_of info,mk_COMB th1 th2 thy)
  1.2247 -	val _ = message "RESULT:"
  1.2248 -	val _ = if_debug pth res
  1.2249 +        val _ = message "COMB:"
  1.2250 +        val _ = if_debug pth hth1
  1.2251 +        val _ = if_debug pth hth2
  1.2252 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2253 +        val res = HOLThm(rens_of info,mk_COMB th1 th2 thy)
  1.2254 +        val _ = message "RESULT:"
  1.2255 +        val _ = if_debug pth res
  1.2256      in
  1.2257 -	(thy,res)
  1.2258 +        (thy,res)
  1.2259      end
  1.2260  
  1.2261  fun TRANS hth1 hth2 thy =
  1.2262      let
  1.2263 -	val _ = message "TRANS:"
  1.2264 -	val _ = if_debug pth hth1
  1.2265 -	val _ = if_debug pth hth2
  1.2266 -	val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2267 -	val th = [th1,th2] MRS trans_thm
  1.2268 -	val res = HOLThm(rens_of info,th)
  1.2269 -	val _ = message "RESULT:"
  1.2270 -	val _ = if_debug pth res
  1.2271 +        val _ = message "TRANS:"
  1.2272 +        val _ = if_debug pth hth1
  1.2273 +        val _ = if_debug pth hth2
  1.2274 +        val (info,[th1,th2]) = disamb_thms [hth1,hth2]
  1.2275 +        val th = [th1,th2] MRS trans_thm
  1.2276 +        val res = HOLThm(rens_of info,th)
  1.2277 +        val _ = message "RESULT:"
  1.2278 +        val _ = if_debug pth res
  1.2279      in
  1.2280 -	(thy,res)
  1.2281 +        (thy,res)
  1.2282      end
  1.2283  
  1.2284  
  1.2285  fun CCONTR tm hth thy =
  1.2286      let
  1.2287 -	val _ = message "SPEC:"
  1.2288 -	val _ = if_debug prin tm
  1.2289 -	val _ = if_debug pth hth
  1.2290 -	val (info,th) = disamb_thm hth
  1.2291 -	val (info',tm') = disamb_term_from info tm
  1.2292 -	val th = norm_hyps th
  1.2293 -	val ct = cterm_of thy tm'
  1.2294 -	val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
  1.2295 -	val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
  1.2296 -	val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
  1.2297 -	val res = HOLThm(rens_of info',res1)
  1.2298 -	val _ = message "RESULT:"
  1.2299 -	val _ = if_debug pth res
  1.2300 +        val _ = message "SPEC:"
  1.2301 +        val _ = if_debug prin tm
  1.2302 +        val _ = if_debug pth hth
  1.2303 +        val (info,th) = disamb_thm hth
  1.2304 +        val (info',tm') = disamb_term_from info tm
  1.2305 +        val th = norm_hyps th
  1.2306 +        val ct = cterm_of thy tm'
  1.2307 +        val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
  1.2308 +        val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
  1.2309 +        val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
  1.2310 +        val res = HOLThm(rens_of info',res1)
  1.2311 +        val _ = message "RESULT:"
  1.2312 +        val _ = if_debug pth res
  1.2313      in
  1.2314 -	(thy,res)
  1.2315 +        (thy,res)
  1.2316      end
  1.2317  
  1.2318  fun mk_ABS v th thy =
  1.2319      let
  1.2320 -	val cv = cterm_of thy v
  1.2321 -	val th1 = implies_elim_all (beta_eta_thm th)
  1.2322 -	val (f,g) = case concl_of th1 of
  1.2323 -			_ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
  1.2324 -		      | _ => raise ERR "mk_ABS" "Bad conclusion"
  1.2325 -	val (fd,fr) = dom_rng (type_of f)
  1.2326 -	val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
  1.2327 -	val th2 = forall_intr cv th1
  1.2328 -	val th3 = th2 COMP abs_thm'
  1.2329 -	val res = implies_intr_hyps th3
  1.2330 +        val cv = cterm_of thy v
  1.2331 +        val th1 = implies_elim_all (beta_eta_thm th)
  1.2332 +        val (f,g) = case concl_of th1 of
  1.2333 +                        _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
  1.2334 +                      | _ => raise ERR "mk_ABS" "Bad conclusion"
  1.2335 +        val (fd,fr) = dom_rng (type_of f)
  1.2336 +        val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
  1.2337 +        val th2 = forall_intr cv th1
  1.2338 +        val th3 = th2 COMP abs_thm'
  1.2339 +        val res = implies_intr_hyps th3
  1.2340      in
  1.2341 -	res
  1.2342 +        res
  1.2343      end
  1.2344  
  1.2345  fun ABS v hth thy =
  1.2346      let
  1.2347 -	val _ = message "ABS:"
  1.2348 -	val _ = if_debug prin v
  1.2349 -	val _ = if_debug pth hth
  1.2350 -	val (info,th) = disamb_thm hth
  1.2351 -	val (info',v') = disamb_term_from info v
  1.2352 -	val res = HOLThm(rens_of info',mk_ABS v' th thy)
  1.2353 -	val _ = message "RESULT:"
  1.2354 -	val _ = if_debug pth res
  1.2355 +        val _ = message "ABS:"
  1.2356 +        val _ = if_debug prin v
  1.2357 +        val _ = if_debug pth hth
  1.2358 +        val (info,th) = disamb_thm hth
  1.2359 +        val (info',v') = disamb_term_from info v
  1.2360 +        val res = HOLThm(rens_of info',mk_ABS v' th thy)
  1.2361 +        val _ = message "RESULT:"
  1.2362 +        val _ = if_debug pth res
  1.2363      in
  1.2364 -	(thy,res)
  1.2365 +        (thy,res)
  1.2366      end
  1.2367  
  1.2368  fun GEN_ABS copt vlist hth thy =
  1.2369      let
  1.2370 -	val _ = message "GEN_ABS:"
  1.2371 -	val _ = case copt of
  1.2372 -		    SOME c => if_debug prin c
  1.2373 -		  | NONE => ()
  1.2374 -	val _ = if_debug (app prin) vlist
  1.2375 -	val _ = if_debug pth hth
  1.2376 -	val (info,th) = disamb_thm hth
  1.2377 -	val (info',vlist') = disamb_terms_from info vlist
  1.2378 -	val th1 =
  1.2379 -	    case copt of
  1.2380 -		SOME (c as Const(cname,cty)) =>
  1.2381 -		let
  1.2382 -		    fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!"
  1.2383 -		      | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty
  1.2384 -							    then ty2
  1.2385 -							    else ty
  1.2386 -		      | inst_type ty1 ty2 (ty as Type(name,tys)) =
  1.2387 -			Type(name,map (inst_type ty1 ty2) tys)
  1.2388 -		in
  1.2389 -		    foldr (fn (v,th) =>
  1.2390 -			      let
  1.2391 -				  val cdom = fst (dom_rng (fst (dom_rng cty)))
  1.2392 -				  val vty  = type_of v
  1.2393 -				  val newcty = inst_type cdom vty cty
  1.2394 -				  val cc = cterm_of thy (Const(cname,newcty))
  1.2395 -			      in
  1.2396 -				  mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
  1.2397 -			      end) th vlist'
  1.2398 -		end
  1.2399 -	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
  1.2400 -	      | NONE =>
  1.2401 -		foldr (fn (v,th) => mk_ABS v th thy) th vlist'
  1.2402 -	val res = HOLThm(rens_of info',th1)
  1.2403 -	val _ = message "RESULT:"
  1.2404 -	val _ = if_debug pth res
  1.2405 +        val _ = message "GEN_ABS:"
  1.2406 +        val _ = case copt of
  1.2407 +                    SOME c => if_debug prin c
  1.2408 +                  | NONE => ()
  1.2409 +        val _ = if_debug (app prin) vlist
  1.2410 +        val _ = if_debug pth hth
  1.2411 +        val (info,th) = disamb_thm hth
  1.2412 +        val (info',vlist') = disamb_terms_from info vlist
  1.2413 +        val th1 =
  1.2414 +            case copt of
  1.2415 +                SOME (c as Const(cname,cty)) =>
  1.2416 +                let
  1.2417 +                    fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!"
  1.2418 +                      | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty
  1.2419 +                                                            then ty2
  1.2420 +                                                            else ty
  1.2421 +                      | inst_type ty1 ty2 (ty as Type(name,tys)) =
  1.2422 +                        Type(name,map (inst_type ty1 ty2) tys)
  1.2423 +                in
  1.2424 +                    foldr (fn (v,th) =>
  1.2425 +                              let
  1.2426 +                                  val cdom = fst (dom_rng (fst (dom_rng cty)))
  1.2427 +                                  val vty  = type_of v
  1.2428 +                                  val newcty = inst_type cdom vty cty
  1.2429 +                                  val cc = cterm_of thy (Const(cname,newcty))
  1.2430 +                              in
  1.2431 +                                  mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
  1.2432 +                              end) th vlist'
  1.2433 +                end
  1.2434 +              | SOME _ => raise ERR "GEN_ABS" "Bad constant"
  1.2435 +              | NONE =>
  1.2436 +                foldr (fn (v,th) => mk_ABS v th thy) th vlist'
  1.2437 +        val res = HOLThm(rens_of info',th1)
  1.2438 +        val _ = message "RESULT:"
  1.2439 +        val _ = if_debug pth res
  1.2440      in
  1.2441 -	(thy,res)
  1.2442 +        (thy,res)
  1.2443      end
  1.2444  
  1.2445  fun NOT_INTRO (hth as HOLThm(rens,th)) thy =
  1.2446      let
  1.2447 -	val _ = message "NOT_INTRO:"
  1.2448 -	val _ = if_debug pth hth
  1.2449 -	val th1 = implies_elim_all (beta_eta_thm th)
  1.2450 -	val a = case concl_of th1 of
  1.2451 -		    _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
  1.2452 -		  | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
  1.2453 -	val ca = cterm_of thy a
  1.2454 -	val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
  1.2455 -	val res = HOLThm(rens,implies_intr_hyps th2)
  1.2456 -	val _ = message "RESULT:"
  1.2457 -	val _ = if_debug pth res
  1.2458 +        val _ = message "NOT_INTRO:"
  1.2459 +        val _ = if_debug pth hth
  1.2460 +        val th1 = implies_elim_all (beta_eta_thm th)
  1.2461 +        val a = case concl_of th1 of
  1.2462 +                    _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
  1.2463 +                  | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
  1.2464 +        val ca = cterm_of thy a
  1.2465 +        val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
  1.2466 +        val res = HOLThm(rens,implies_intr_hyps th2)
  1.2467 +        val _ = message "RESULT:"
  1.2468 +        val _ = if_debug pth res
  1.2469      in
  1.2470 -	(thy,res)
  1.2471 +        (thy,res)
  1.2472      end
  1.2473  
  1.2474  fun NOT_ELIM (hth as HOLThm(rens,th)) thy =
  1.2475      let
  1.2476 -	val _ = message "NOT_INTRO:"
  1.2477 -	val _ = if_debug pth hth
  1.2478 -	val th1 = implies_elim_all (beta_eta_thm th)
  1.2479 -	val a = case concl_of th1 of
  1.2480 -		    _ $ (Const("Not",_) $ a) => a
  1.2481 -		  | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
  1.2482 -	val ca = cterm_of thy a
  1.2483 -	val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
  1.2484 -	val res = HOLThm(rens,implies_intr_hyps th2)
  1.2485 -	val _ = message "RESULT:"
  1.2486 -	val _ = if_debug pth res
  1.2487 +        val _ = message "NOT_INTRO:"
  1.2488 +        val _ = if_debug pth hth
  1.2489 +        val th1 = implies_elim_all (beta_eta_thm th)
  1.2490 +        val a = case concl_of th1 of
  1.2491 +                    _ $ (Const("Not",_) $ a) => a
  1.2492 +                  | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
  1.2493 +        val ca = cterm_of thy a
  1.2494 +        val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
  1.2495 +        val res = HOLThm(rens,implies_intr_hyps th2)
  1.2496 +        val _ = message "RESULT:"
  1.2497 +        val _ = if_debug pth res
  1.2498      in
  1.2499 -	(thy,res)
  1.2500 +        (thy,res)
  1.2501      end
  1.2502  
  1.2503  fun DISCH tm hth thy =
  1.2504      let
  1.2505 -	val _ = message "DISCH:"
  1.2506 -	val _ = if_debug prin tm
  1.2507 -	val _ = if_debug pth hth
  1.2508 -	val (info,th) = disamb_thm hth
  1.2509 -	val (info',tm') = disamb_term_from info tm
  1.2510 -	val prems = prems_of th
  1.2511 -	val th1 = beta_eta_thm th
  1.2512 -	val th2 = implies_elim_all th1
  1.2513 -	val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
  1.2514 -	val th4 = th3 COMP disch_thm
  1.2515 -	val res = HOLThm(rens_of info',implies_intr_hyps th4)
  1.2516 -	val _ = message "RESULT:"
  1.2517 -	val _ = if_debug pth res
  1.2518 +        val _ = message "DISCH:"
  1.2519 +        val _ = if_debug prin tm
  1.2520 +        val _ = if_debug pth hth
  1.2521 +        val (info,th) = disamb_thm hth
  1.2522 +        val (info',tm') = disamb_term_from info tm
  1.2523 +        val prems = prems_of th
  1.2524 +        val th1 = beta_eta_thm th
  1.2525 +        val th2 = implies_elim_all th1
  1.2526 +        val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
  1.2527 +        val th4 = th3 COMP disch_thm
  1.2528 +        val res = HOLThm(rens_of info',implies_intr_hyps th4)
  1.2529 +        val _ = message "RESULT:"
  1.2530 +        val _ = if_debug pth res
  1.2531      in
  1.2532 -	(thy,res)
  1.2533 +        (thy,res)
  1.2534      end
  1.2535  
  1.2536  val spaces = String.concat o separate " "
  1.2537  
  1.2538  fun new_definition thyname constname rhs thy =
  1.2539      let
  1.2540 -	val constname = rename_const thyname thy constname
  1.2541 +        val constname = rename_const thyname thy constname
  1.2542          val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
  1.2543 -	val _ = warning ("Introducing constant " ^ constname)
  1.2544 -	val (thmname,thy) = get_defname thyname constname thy
  1.2545 -	val (info,rhs') = disamb_term rhs
  1.2546 -	val ctype = type_of rhs'
  1.2547 -	val csyn = mk_syn thy constname
  1.2548 -	val thy1 = case HOL4DefThy.get thy of
  1.2549 -		       Replaying _ => thy
  1.2550 -		     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
  1.2551 -	val eq = mk_defeq constname rhs' thy1
  1.2552 -	val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
  1.2553 -	val _ = ImportRecorder.add_defs thmname eq
  1.2554 -	val def_thm = hd thms
  1.2555 -	val thm' = def_thm RS meta_eq_to_obj_eq_thm
  1.2556 -	val (thy',th) = (thy2, thm')
  1.2557 -	val fullcname = Sign.intern_const thy' constname
  1.2558 -	val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
  1.2559 -	val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
  1.2560 -	val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
  1.2561 -	val rew = rewrite_hol4_term eq thy''
  1.2562 -	val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
  1.2563 -	val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
  1.2564 -		    then
  1.2565 -			let
  1.2566 -			    val p1 = quotename constname
  1.2567 -			    val p2 = string_of_ctyp (ctyp_of thy'' ctype)
  1.2568 -			    val p3 = string_of_mixfix csyn
  1.2569 -			    val p4 = smart_string_of_cterm crhs
  1.2570 -			in
  1.2571 -			    add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
  1.2572 -			end
  1.2573 -		    else
  1.2574 -			(add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
  1.2575 -				   "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
  1.2576 -				  thy'')
  1.2577 -	val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
  1.2578 -		      SOME (_,res) => HOLThm(rens_of linfo,res)
  1.2579 -		    | NONE => raise ERR "new_definition" "Bad conclusion"
  1.2580 -	val fullname = Sign.full_name thy22 thmname
  1.2581 -	val thy22' = case opt_get_output_thy thy22 of
  1.2582 -			 "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
  1.2583 -				add_hol4_mapping thyname thmname fullname thy22)
  1.2584 -		       | output_thy =>
  1.2585 -			 let
  1.2586 -			     val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
  1.2587 -			     val _ = ImportRecorder.add_hol_move fullname moved_thmname
  1.2588 -			     val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
  1.2589 -			 in
  1.2590 -			     thy22 |> add_hol4_move fullname moved_thmname
  1.2591 -				   |> add_hol4_mapping thyname thmname moved_thmname
  1.2592 -			 end
  1.2593 -	val _ = message "new_definition:"
  1.2594 -	val _ = if_debug pth hth
  1.2595 +        val _ = warning ("Introducing constant " ^ constname)
  1.2596 +        val (thmname,thy) = get_defname thyname constname thy
  1.2597 +        val (info,rhs') = disamb_term rhs
  1.2598 +        val ctype = type_of rhs'
  1.2599 +        val csyn = mk_syn thy constname
  1.2600 +        val thy1 = case HOL4DefThy.get thy of
  1.2601 +                       Replaying _ => thy
  1.2602 +                     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
  1.2603 +        val eq = mk_defeq constname rhs' thy1
  1.2604 +        val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
  1.2605 +        val _ = ImportRecorder.add_defs thmname eq
  1.2606 +        val def_thm = hd thms
  1.2607 +        val thm' = def_thm RS meta_eq_to_obj_eq_thm
  1.2608 +        val (thy',th) = (thy2, thm')
  1.2609 +        val fullcname = Sign.intern_const thy' constname
  1.2610 +        val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
  1.2611 +        val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
  1.2612 +        val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
  1.2613 +        val rew = rewrite_hol4_term eq thy''
  1.2614 +        val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
  1.2615 +        val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
  1.2616 +                    then
  1.2617 +                        let
  1.2618 +                            val p1 = quotename constname
  1.2619 +                            val p2 = string_of_ctyp (ctyp_of thy'' ctype)
  1.2620 +                            val p3 = string_of_mixfix csyn
  1.2621 +                            val p4 = smart_string_of_cterm crhs
  1.2622 +                        in
  1.2623 +                            add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
  1.2624 +                        end
  1.2625 +                    else
  1.2626 +                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
  1.2627 +                                   "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
  1.2628 +                                  thy'')
  1.2629 +        val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
  1.2630 +                      SOME (_,res) => HOLThm(rens_of linfo,res)
  1.2631 +                    | NONE => raise ERR "new_definition" "Bad conclusion"
  1.2632 +        val fullname = Sign.full_name thy22 thmname
  1.2633 +        val thy22' = case opt_get_output_thy thy22 of
  1.2634 +                         "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
  1.2635 +                                add_hol4_mapping thyname thmname fullname thy22)
  1.2636 +                       | output_thy =>
  1.2637 +                         let
  1.2638 +                             val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
  1.2639 +                             val _ = ImportRecorder.add_hol_move fullname moved_thmname
  1.2640 +                             val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
  1.2641 +                         in
  1.2642 +                             thy22 |> add_hol4_move fullname moved_thmname
  1.2643 +                                   |> add_hol4_mapping thyname thmname moved_thmname
  1.2644 +                         end
  1.2645 +        val _ = message "new_definition:"
  1.2646 +        val _ = if_debug pth hth
  1.2647      in
  1.2648 -	(thy22',hth)
  1.2649 +        (thy22',hth)
  1.2650      end
  1.2651      handle e => (message "exception in new_definition"; print_exn e)
  1.2652  
  1.2653 @@ -1983,81 +1985,81 @@
  1.2654  in
  1.2655  fun new_specification thyname thmname names hth thy =
  1.2656      case HOL4DefThy.get thy of
  1.2657 -	Replaying _ => (thy,hth)
  1.2658 +        Replaying _ => (thy,hth)
  1.2659        | _ =>
  1.2660 -	let
  1.2661 -	    val _ = message "NEW_SPEC:"
  1.2662 -	    val _ = if_debug pth hth
  1.2663 -	    val names = map (rename_const thyname thy) names
  1.2664 -	    val _ = warning ("Introducing constants " ^ commas names)
  1.2665 -	    val (HOLThm(rens,th)) = norm_hthm thy hth
  1.2666 -	    val thy1 = case HOL4DefThy.get thy of
  1.2667 -			   Replaying _ => thy
  1.2668 -			 | _ =>
  1.2669 -			   let
  1.2670 -			       fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
  1.2671 -				 | dest_eta_abs body =
  1.2672 -				   let
  1.2673 -				       val (dT,rT) = dom_rng (type_of body)
  1.2674 -				   in
  1.2675 -				       ("x",dT,body $ Bound 0)
  1.2676 -				   end
  1.2677 -				   handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
  1.2678 -			       fun dest_exists (Const("Ex",_) $ abody) =
  1.2679 -				   dest_eta_abs abody
  1.2680 -				 | dest_exists tm =
  1.2681 -				   raise ERR "new_specification" "Bad existential formula"
  1.2682 +        let
  1.2683 +            val _ = message "NEW_SPEC:"
  1.2684 +            val _ = if_debug pth hth
  1.2685 +            val names = map (rename_const thyname thy) names
  1.2686 +            val _ = warning ("Introducing constants " ^ commas names)
  1.2687 +            val (HOLThm(rens,th)) = norm_hthm thy hth
  1.2688 +            val thy1 = case HOL4DefThy.get thy of
  1.2689 +                           Replaying _ => thy
  1.2690 +                         | _ =>
  1.2691 +                           let
  1.2692 +                               fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
  1.2693 +                                 | dest_eta_abs body =
  1.2694 +                                   let
  1.2695 +                                       val (dT,rT) = dom_rng (type_of body)
  1.2696 +                                   in
  1.2697 +                                       ("x",dT,body $ Bound 0)
  1.2698 +                                   end
  1.2699 +                                   handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
  1.2700 +                               fun dest_exists (Const("Ex",_) $ abody) =
  1.2701 +                                   dest_eta_abs abody
  1.2702 +                                 | dest_exists tm =
  1.2703 +                                   raise ERR "new_specification" "Bad existential formula"
  1.2704  
  1.2705 -			       val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
  1.2706 -							  let
  1.2707 -							      val (_,cT,p) = dest_exists ex
  1.2708 -							  in
  1.2709 -							      ((cname,cT,mk_syn thy cname)::cs,p)
  1.2710 -							  end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
  1.2711 -			       val str = Library.foldl (fn (acc,(c,T,csyn)) =>
  1.2712 -						   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
  1.2713 -			       val thy' = add_dump str thy
  1.2714 -			       val _ = ImportRecorder.add_consts consts
  1.2715 -			   in
  1.2716 -			       Sign.add_consts_i consts thy'
  1.2717 -			   end
  1.2718 +                               val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
  1.2719 +                                                          let
  1.2720 +                                                              val (_,cT,p) = dest_exists ex
  1.2721 +                                                          in
  1.2722 +                                                              ((cname,cT,mk_syn thy cname)::cs,p)
  1.2723 +                                                          end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
  1.2724 +                               val str = Library.foldl (fn (acc,(c,T,csyn)) =>
  1.2725 +                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
  1.2726 +                               val thy' = add_dump str thy
  1.2727 +                               val _ = ImportRecorder.add_consts consts
  1.2728 +                           in
  1.2729 +                               Sign.add_consts_i consts thy'
  1.2730 +                           end
  1.2731  
  1.2732 -	    val thy1 = foldr (fn(name,thy)=>
  1.2733 -				snd (get_defname thyname name thy)) thy1 names
  1.2734 -	    fun new_name name = fst (get_defname thyname name thy1)
  1.2735 -	    val names' = map (fn name => (new_name name,name,false)) names
  1.2736 -	    val (thy',res) = SpecificationPackage.add_specification NONE
  1.2737 -				 names'
  1.2738 -				 (thy1,th)
  1.2739 -	    val _ = ImportRecorder.add_specification names' th
  1.2740 -	    val res' = Thm.unvarify res
  1.2741 -	    val hth = HOLThm(rens,res')
  1.2742 -	    val rew = rewrite_hol4_term (concl_of res') thy'
  1.2743 -	    val th  = equal_elim rew res'
  1.2744 -	    fun handle_const (name,thy) =
  1.2745 -		let
  1.2746 -		    val defname = def_name name
  1.2747 -		    val (newname,thy') = get_defname thyname name thy
  1.2748 -		in
  1.2749 -		    (if defname = newname
  1.2750 -		     then quotename name
  1.2751 -		     else (quotename newname) ^ ": " ^ (quotename name),thy')
  1.2752 -		end
  1.2753 -	    val (new_names,thy') = foldr (fn(name,(names,thy)) =>
  1.2754 -					    let
  1.2755 -						val (name',thy') = handle_const (name,thy)
  1.2756 -					    in
  1.2757 -						(name'::names,thy')
  1.2758 -					    end) ([],thy') names
  1.2759 -	    val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
  1.2760 -				  "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
  1.2761 -				 thy'
  1.2762 -	    val _ = message "RESULT:"
  1.2763 -	    val _ = if_debug pth hth
  1.2764 -	in
  1.2765 -	    intern_store_thm false thyname thmname hth thy''
  1.2766 -	end
  1.2767 -	handle e => (message "exception in new_specification"; print_exn e)
  1.2768 +            val thy1 = foldr (fn(name,thy)=>
  1.2769 +                                snd (get_defname thyname name thy)) thy1 names
  1.2770 +            fun new_name name = fst (get_defname thyname name thy1)
  1.2771 +            val names' = map (fn name => (new_name name,name,false)) names
  1.2772 +            val (thy',res) = SpecificationPackage.add_specification NONE
  1.2773 +                                 names'
  1.2774 +                                 (thy1,th)
  1.2775 +            val _ = ImportRecorder.add_specification names' th
  1.2776 +            val res' = Thm.unvarify res
  1.2777 +            val hth = HOLThm(rens,res')
  1.2778 +            val rew = rewrite_hol4_term (concl_of res') thy'
  1.2779 +            val th  = equal_elim rew res'
  1.2780 +            fun handle_const (name,thy) =
  1.2781 +                let
  1.2782 +                    val defname = def_name name
  1.2783 +                    val (newname,thy') = get_defname thyname name thy
  1.2784 +                in
  1.2785 +                    (if defname = newname
  1.2786 +                     then quotename name
  1.2787 +                     else (quotename newname) ^ ": " ^ (quotename name),thy')
  1.2788 +                end
  1.2789 +            val (new_names,thy') = foldr (fn(name,(names,thy)) =>
  1.2790 +                                            let
  1.2791 +                                                val (name',thy') = handle_const (name,thy)
  1.2792 +                                            in
  1.2793 +                                                (name'::names,thy')
  1.2794 +                                            end) ([],thy') names
  1.2795 +            val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
  1.2796 +                                  "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
  1.2797 +                                 thy'
  1.2798 +            val _ = message "RESULT:"
  1.2799 +            val _ = if_debug pth hth
  1.2800 +        in
  1.2801 +            intern_store_thm false thyname thmname hth thy''
  1.2802 +        end
  1.2803 +        handle e => (message "exception in new_specification"; print_exn e)
  1.2804  
  1.2805  end
  1.2806  
  1.2807 @@ -2065,9 +2067,9 @@
  1.2808  
  1.2809  fun to_isa_thm (hth as HOLThm(_,th)) =
  1.2810      let
  1.2811 -	val (HOLThm args) = norm_hthm (theory_of_thm th) hth
  1.2812 +        val (HOLThm args) = norm_hthm (theory_of_thm th) hth
  1.2813      in
  1.2814 -	apsnd strip_shyps args
  1.2815 +        apsnd strip_shyps args
  1.2816      end
  1.2817  
  1.2818  fun to_isa_term tm = tm
  1.2819 @@ -2080,74 +2082,74 @@
  1.2820  in
  1.2821  fun new_type_definition thyname thmname tycname hth thy =
  1.2822      case HOL4DefThy.get thy of
  1.2823 -	Replaying _ => (thy,hth)
  1.2824 +        Replaying _ => (thy,hth)
  1.2825        | _ =>
  1.2826 -	let
  1.2827 -	    val _ = message "TYPE_DEF:"
  1.2828 -	    val _ = if_debug pth hth
  1.2829 -	    val _ = warning ("Introducing type " ^ tycname)
  1.2830 -	    val (HOLThm(rens,td_th)) = norm_hthm thy hth
  1.2831 -	    val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
  1.2832 -	    val c = case concl_of th2 of
  1.2833 -			_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
  1.2834 -		      | _ => raise ERR "new_type_definition" "Bad type definition theorem"
  1.2835 -	    val tfrees = term_tfrees c
  1.2836 -	    val tnames = map fst tfrees
  1.2837 -	    val tsyn = mk_syn thy tycname
  1.2838 -	    val typ = (tycname,tnames,tsyn)
  1.2839 -	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
  1.2840 +        let
  1.2841 +            val _ = message "TYPE_DEF:"
  1.2842 +            val _ = if_debug pth hth
  1.2843 +            val _ = warning ("Introducing type " ^ tycname)
  1.2844 +            val (HOLThm(rens,td_th)) = norm_hthm thy hth
  1.2845 +            val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
  1.2846 +            val c = case concl_of th2 of
  1.2847 +                        _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
  1.2848 +                      | _ => raise ERR "new_type_definition" "Bad type definition theorem"
  1.2849 +            val tfrees = term_tfrees c
  1.2850 +            val tnames = map fst tfrees
  1.2851 +            val tsyn = mk_syn thy tycname
  1.2852 +            val typ = (tycname,tnames,tsyn)
  1.2853 +            val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
  1.2854              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
  1.2855  
  1.2856 -	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
  1.2857 +            val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
  1.2858  
  1.2859 -	    val fulltyname = Sign.intern_type thy' tycname
  1.2860 -	    val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
  1.2861 -	    val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
  1.2862 +            val fulltyname = Sign.intern_type thy' tycname
  1.2863 +            val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
  1.2864 +            val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
  1.2865  
  1.2866 -	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
  1.2867 -	    val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
  1.2868 -		    else ()
  1.2869 -	    val thy4 = add_hol4_pending thyname thmname args thy''
  1.2870 -	    val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
  1.2871 +            val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
  1.2872 +            val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
  1.2873 +                    else ()
  1.2874 +            val thy4 = add_hol4_pending thyname thmname args thy''
  1.2875 +            val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
  1.2876  
  1.2877 -	    val rew = rewrite_hol4_term (concl_of td_th) thy4
  1.2878 -	    val th  = equal_elim rew (Thm.transfer thy4 td_th)
  1.2879 -	    val c   = case HOLogic.dest_Trueprop (prop_of th) of
  1.2880 -			  Const("Ex",exT) $ P =>
  1.2881 -			  let
  1.2882 -			      val PT = domain_type exT
  1.2883 -			  in
  1.2884 -			      Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
  1.2885 -			  end
  1.2886 -			| _ => error "Internal error in ProofKernel.new_typedefinition"
  1.2887 -	    val tnames_string = if null tnames
  1.2888 -				then ""
  1.2889 -				else "(" ^ commas tnames ^ ") "
  1.2890 -	    val proc_prop = if null tnames
  1.2891 -			    then smart_string_of_cterm
  1.2892 -			    else Library.setmp show_all_types true smart_string_of_cterm
  1.2893 -	    val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
  1.2894 -				 ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
  1.2895 +            val rew = rewrite_hol4_term (concl_of td_th) thy4
  1.2896 +            val th  = equal_elim rew (Thm.transfer thy4 td_th)
  1.2897 +            val c   = case HOLogic.dest_Trueprop (prop_of th) of
  1.2898 +                          Const("Ex",exT) $ P =>
  1.2899 +                          let
  1.2900 +                              val PT = domain_type exT
  1.2901 +                          in
  1.2902 +                              Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
  1.2903 +                          end
  1.2904 +                        | _ => error "Internal error in ProofKernel.new_typedefinition"
  1.2905 +            val tnames_string = if null tnames
  1.2906 +                                then ""
  1.2907 +                                else "(" ^ commas tnames ^ ") "
  1.2908 +            val proc_prop = if null tnames
  1.2909 +                            then smart_string_of_cterm
  1.2910 +                            else Library.setmp show_all_types true smart_string_of_cterm
  1.2911 +            val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
  1.2912 +                                 ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
  1.2913  
  1.2914 -	    val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
  1.2915 +            val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
  1.2916  
  1.2917 -	    val _ = message "RESULT:"
  1.2918 -	    val _ = if_debug pth hth'
  1.2919 -	in
  1.2920 -	    (thy6,hth')
  1.2921 -	end
  1.2922 -	handle e => (message "exception in new_type_definition"; print_exn e)
  1.2923 +            val _ = message "RESULT:"
  1.2924 +            val _ = if_debug pth hth'
  1.2925 +        in
  1.2926 +            (thy6,hth')
  1.2927 +        end
  1.2928 +        handle e => (message "exception in new_type_definition"; print_exn e)
  1.2929  
  1.2930  fun add_dump_constdefs thy defname constname rhs ty =
  1.2931      let
  1.2932 -	val n = quotename constname
  1.2933 -	val t = string_of_ctyp (ctyp_of thy ty)
  1.2934 -	val syn = string_of_mixfix (mk_syn thy constname)
  1.2935 -	(*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
  1.2936 +        val n = quotename constname
  1.2937 +        val t = string_of_ctyp (ctyp_of thy ty)
  1.2938 +        val syn = string_of_mixfix (mk_syn thy constname)
  1.2939 +        (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
  1.2940          val eq = quote (constname ^ " == "^rhs)
  1.2941 -	val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
  1.2942 +        val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
  1.2943      in
  1.2944 -	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy
  1.2945 +        add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy
  1.2946      end
  1.2947  
  1.2948  fun add_dump_syntax thy name =
  1.2949 @@ -2160,85 +2162,85 @@
  1.2950  
  1.2951  fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
  1.2952      case HOL4DefThy.get thy of
  1.2953 -	Replaying _ => (thy,
  1.2954 +        Replaying _ => (thy,
  1.2955            HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
  1.2956        | _ =>
  1.2957 -	let
  1.2958 +        let
  1.2959              val _ = message "TYPE_INTRO:"
  1.2960 -	    val _ = if_debug pth hth
  1.2961 -	    val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
  1.2962 -	    val (HOLThm(rens,td_th)) = norm_hthm thy hth
  1.2963 -	    val tT = type_of t
  1.2964 -	    val light_nonempty' =
  1.2965 -		Drule.instantiate' [SOME (ctyp_of thy tT)]
  1.2966 -				   [SOME (cterm_of thy P),
  1.2967 -				    SOME (cterm_of thy t)] light_nonempty
  1.2968 -	    val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
  1.2969 -	    val c = case concl_of th2 of
  1.2970 -			_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
  1.2971 -		      | _ => raise ERR "type_introduction" "Bad type definition theorem"
  1.2972 -	    val tfrees = term_tfrees c
  1.2973 -	    val tnames = sort string_ord (map fst tfrees)
  1.2974 -	    val tsyn = mk_syn thy tycname
  1.2975 -	    val typ = (tycname,tnames,tsyn)
  1.2976 -	    val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
  1.2977 -	    val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
  1.2978 -	    val fulltyname = Sign.intern_type thy' tycname
  1.2979 -	    val aty = Type (fulltyname, map mk_vartype tnames)
  1.2980 -	    val abs_ty = tT --> aty
  1.2981 -	    val rep_ty = aty --> tT
  1.2982 +            val _ = if_debug pth hth
  1.2983 +            val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
  1.2984 +            val (HOLThm(rens,td_th)) = norm_hthm thy hth
  1.2985 +            val tT = type_of t
  1.2986 +            val light_nonempty' =
  1.2987 +                Drule.instantiate' [SOME (ctyp_of thy tT)]
  1.2988 +                                   [SOME (cterm_of thy P),
  1.2989 +                                    SOME (cterm_of thy t)] light_nonempty
  1.2990 +            val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
  1.2991 +            val c = case concl_of th2 of
  1.2992 +                        _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
  1.2993 +                      | _ => raise ERR "type_introduction" "Bad type definition theorem"
  1.2994 +            val tfrees = term_tfrees c
  1.2995 +            val tnames = sort string_ord (map fst tfrees)
  1.2996 +            val tsyn = mk_syn thy tycname
  1.2997 +            val typ = (tycname,tnames,tsyn)
  1.2998 +            val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
  1.2999 +            val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
  1.3000 +            val fulltyname = Sign.intern_type thy' tycname
  1.3001 +            val aty = Type (fulltyname, map mk_vartype tnames)
  1.3002 +            val abs_ty = tT --> aty
  1.3003 +            val rep_ty = aty --> tT
  1.3004              val typedef_hol2hollight' =
  1.3005 -		Drule.instantiate'
  1.3006 -		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
  1.3007 -		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
  1.3008 +                Drule.instantiate'
  1.3009 +                    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
  1.3010 +                    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
  1.3011                      typedef_hol2hollight
  1.3012 -	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
  1.3013 +            val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
  1.3014              val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
  1.3015                raise ERR "type_introduction" "no type variables expected any more"
  1.3016              val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
  1.3017                raise ERR "type_introduction" "no term variables expected any more"
  1.3018 -	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
  1.3019 +            val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
  1.3020              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
  1.3021 -	    val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
  1.3022 +            val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
  1.3023              val _ = message "step 4"
  1.3024 -	    val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
  1.3025 -	    val thy4 = add_hol4_pending thyname thmname args thy''
  1.3026 -	    val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
  1.3027 +            val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
  1.3028 +            val thy4 = add_hol4_pending thyname thmname args thy''
  1.3029 +            val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
  1.3030  
  1.3031 -	    val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
  1.3032 -	    val c   =
  1.3033 -		let
  1.3034 -		    val PT = type_of P'
  1.3035 -		in
  1.3036 -		    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
  1.3037 -		end
  1.3038 +            val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
  1.3039 +            val c   =
  1.3040 +                let
  1.3041 +                    val PT = type_of P'
  1.3042 +                in
  1.3043 +                    Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
  1.3044 +                end
  1.3045  
  1.3046 -	    val tnames_string = if null tnames
  1.3047 -				then ""
  1.3048 -				else "(" ^ commas tnames ^ ") "
  1.3049 -	    val proc_prop = if null tnames
  1.3050 -			    then smart_string_of_cterm
  1.3051 -			    else Library.setmp show_all_types true smart_string_of_cterm
  1.3052 -	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
  1.3053 +            val tnames_string = if null tnames
  1.3054 +                                then ""
  1.3055 +                                else "(" ^ commas tnames ^ ") "
  1.3056 +            val proc_prop = if null tnames
  1.3057 +                            then smart_string_of_cterm
  1.3058 +                            else Library.setmp show_all_types true smart_string_of_cterm
  1.3059 +            val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
  1.3060                " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
  1.3061 -	      (string_of_mixfix tsyn) ^ " morphisms "^
  1.3062 +              (string_of_mixfix tsyn) ^ " morphisms "^
  1.3063                (quote rep_name)^" "^(quote abs_name)^"\n"^
  1.3064 -	      ("  apply (rule light_ex_imp_nonempty[where t="^
  1.3065 +              ("  apply (rule light_ex_imp_nonempty[where t="^
  1.3066                (proc_prop (cterm_of thy4 t))^"])\n"^
  1.3067 -	      ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
  1.3068 -	    val str_aty = string_of_ctyp (ctyp_of thy aty)
  1.3069 +              ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
  1.3070 +            val str_aty = string_of_ctyp (ctyp_of thy aty)
  1.3071              val thy = add_dump_syntax thy rep_name
  1.3072              val thy = add_dump_syntax thy abs_name
  1.3073 -	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
  1.3074 +            val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
  1.3075                " = typedef_hol2hollight \n"^
  1.3076                "  [where a=\"a :: "^str_aty^"\" and r=r" ^
  1.3077 -	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
  1.3078 -	    val _ = message "RESULT:"
  1.3079 -	    val _ = if_debug pth hth'
  1.3080 -	in
  1.3081 -	    (thy,hth')
  1.3082 -	end
  1.3083 -	handle e => (message "exception in type_introduction"; print_exn e)
  1.3084 +              " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
  1.3085 +            val _ = message "RESULT:"
  1.3086 +            val _ = if_debug pth hth'
  1.3087 +        in
  1.3088 +            (thy,hth')
  1.3089 +        end
  1.3090 +        handle e => (message "exception in type_introduction"; print_exn e)
  1.3091  end
  1.3092  
  1.3093  val prin = prin
     2.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Thu Apr 10 20:54:18 2008 +0200
     2.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Sat Apr 12 17:00:35 2008 +0200
     2.3 @@ -187,7 +187,10 @@
     2.4   *---------------------------------------------------------------------------*)
     2.5  
     2.6  fun mk_prop ctm =
     2.7 -  let val {t, thy, ...} = Thm.rep_cterm ctm in
     2.8 +  let
     2.9 +    val thy = Thm.theory_of_cterm ctm;
    2.10 +    val t = Thm.term_of ctm;
    2.11 +  in
    2.12      if can HOLogic.dest_Trueprop t then ctm
    2.13      else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
    2.14    end
     3.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Apr 10 20:54:18 2008 +0200
     3.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Apr 12 17:00:35 2008 +0200
     3.3 @@ -93,7 +93,7 @@
     3.4  fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
     3.5  
     3.6  fun join_assums th =
     3.7 -  let val {thy,...} = rep_thm th
     3.8 +  let val thy = Thm.theory_of_thm th
     3.9        val tych = cterm_of thy
    3.10        val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
    3.11        val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
     4.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Apr 10 20:54:18 2008 +0200
     4.2 +++ b/src/HOL/Tools/TFL/rules.ML	Sat Apr 12 17:00:35 2008 +0200
     4.3 @@ -171,7 +171,8 @@
     4.4  (*----------------------------------------------------------------------------
     4.5   *        Disjunction
     4.6   *---------------------------------------------------------------------------*)
     4.7 -local val {prop,thy,...} = rep_thm disjI1
     4.8 +local val thy = Thm.theory_of_thm disjI1
     4.9 +      val prop = Thm.prop_of disjI1
    4.10        val [P,Q] = term_vars prop
    4.11        val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
    4.12  in
    4.13 @@ -179,7 +180,8 @@
    4.14    handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
    4.15  end;
    4.16  
    4.17 -local val {prop,thy,...} = rep_thm disjI2
    4.18 +local val thy = Thm.theory_of_thm disjI2
    4.19 +      val prop = Thm.prop_of disjI2
    4.20        val [P,Q] = term_vars prop
    4.21        val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
    4.22  in
    4.23 @@ -274,17 +276,15 @@
    4.24   *        Universals
    4.25   *---------------------------------------------------------------------------*)
    4.26  local (* this is fragile *)
    4.27 -      val {prop,thy,...} = rep_thm spec
    4.28 +      val thy = Thm.theory_of_thm spec
    4.29 +      val prop = Thm.prop_of spec
    4.30        val x = hd (tl (term_vars prop))
    4.31        val cTV = ctyp_of thy (type_of x)
    4.32        val gspec = forall_intr (cterm_of thy x) spec
    4.33  in
    4.34  fun SPEC tm thm =
    4.35 -   let val {thy,T,...} = rep_cterm tm
    4.36 -       val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec
    4.37 -   in
    4.38 -      thm RS (forall_elim tm gspec')
    4.39 -   end
    4.40 +   let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
    4.41 +   in thm RS (forall_elim tm gspec') end
    4.42  end;
    4.43  
    4.44  fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
    4.45 @@ -293,7 +293,8 @@
    4.46  val ISPECL = fold ISPEC;
    4.47  
    4.48  (* Not optimized! Too complicated. *)
    4.49 -local val {prop,thy,...} = rep_thm allI
    4.50 +local val thy = Thm.theory_of_thm allI
    4.51 +      val prop = Thm.prop_of allI
    4.52        val [P] = add_term_vars (prop, [])
    4.53        fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
    4.54        fun ctm_theta s = map (fn (i, (_, tm2)) =>
    4.55 @@ -306,12 +307,13 @@
    4.56  in
    4.57  fun GEN v th =
    4.58     let val gth = forall_intr v th
    4.59 -       val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth
    4.60 +       val thy = Thm.theory_of_thm gth
    4.61 +       val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
    4.62         val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
    4.63         val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
    4.64         val allI2 = instantiate (certify thy theta) allI
    4.65         val thm = Thm.implies_elim allI2 gth
    4.66 -       val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm
    4.67 +       val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
    4.68         val prop' = tp $ (A $ Abs(x,ty,M))
    4.69     in ALPHA thm (cterm_of thy prop')
    4.70     end
    4.71 @@ -320,7 +322,8 @@
    4.72  val GENL = fold_rev GEN;
    4.73  
    4.74  fun GEN_ALL thm =
    4.75 -   let val {prop,thy,...} = rep_thm thm
    4.76 +   let val thy = Thm.theory_of_thm thm
    4.77 +       val prop = Thm.prop_of thm
    4.78         val tycheck = cterm_of thy
    4.79         val vlist = map tycheck (add_term_vars (prop, []))
    4.80    in GENL vlist thm
    4.81 @@ -352,18 +355,21 @@
    4.82    let
    4.83      val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
    4.84      val redex = D.capply lam fvar
    4.85 -    val {thy, t = t$u,...} = Thm.rep_cterm redex
    4.86 +    val thy = Thm.theory_of_cterm redex
    4.87 +    val t$u = Thm.term_of redex
    4.88      val residue = Thm.cterm_of thy (Term.betapply (t, u))
    4.89    in
    4.90      GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
    4.91        handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
    4.92    end;
    4.93  
    4.94 -local val {prop,thy,...} = rep_thm exI
    4.95 +local val thy = Thm.theory_of_thm exI
    4.96 +      val prop = Thm.prop_of exI
    4.97        val [P,x] = term_vars prop
    4.98  in
    4.99  fun EXISTS (template,witness) thm =
   4.100 -   let val {prop,thy,...} = rep_thm thm
   4.101 +   let val thy = Thm.theory_of_thm thm
   4.102 +       val prop = Thm.prop_of thm
   4.103         val P' = cterm_of thy P
   4.104         val x' = cterm_of thy x
   4.105         val abstr = #2 (D.dest_comb template)
   4.106 @@ -396,16 +402,15 @@
   4.107  (* Could be improved, but needs "subst_free" for certified terms *)
   4.108  
   4.109  fun IT_EXISTS blist th =
   4.110 -   let val {thy,...} = rep_thm th
   4.111 +   let val thy = Thm.theory_of_thm th
   4.112         val tych = cterm_of thy
   4.113 -       val detype = #t o rep_cterm
   4.114 -       val blist' = map (fn (x,y) => (detype x, detype y)) blist
   4.115 +       val blist' = map (pairself Thm.term_of) blist
   4.116         fun ex v M  = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
   4.117  
   4.118    in
   4.119    fold_rev (fn (b as (r1,r2)) => fn thm =>
   4.120          EXISTS(ex r2 (subst_free [b]
   4.121 -                   (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
   4.122 +                   (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)
   4.123                thm)
   4.124         blist' th
   4.125    end;
   4.126 @@ -451,13 +456,10 @@
   4.127  
   4.128  (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   4.129  fun is_cong thm =
   4.130 -  let val {prop, ...} = rep_thm thm
   4.131 -  in case prop
   4.132 +  case (Thm.prop_of thm)
   4.133       of (Const("==>",_)$(Const("Trueprop",_)$ _) $
   4.134           (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
   4.135 -      | _ => true
   4.136 -  end;
   4.137 -
   4.138 +      | _ => true;
   4.139  
   4.140  
   4.141  fun dest_equal(Const ("==",_) $
   4.142 @@ -521,9 +523,9 @@
   4.143  
   4.144  (* Note: rename_params_rule counts from 1, not 0 *)
   4.145  fun rename thm =
   4.146 -  let val {prop,thy,...} = rep_thm thm
   4.147 +  let val thy = Thm.theory_of_thm thm
   4.148        val tych = cterm_of thy
   4.149 -      val ants = Logic.strip_imp_prems prop
   4.150 +      val ants = Logic.strip_imp_prems (Thm.prop_of thm)
   4.151        val news = get (ants,1,[])
   4.152    in
   4.153    fold rename_params_rule news thm
   4.154 @@ -745,12 +747,12 @@
   4.155                end end
   4.156  
   4.157               fun eliminate thm =
   4.158 -               case (rep_thm thm)
   4.159 -               of {prop = (Const("==>",_) $ imp $ _), thy, ...} =>
   4.160 +               case Thm.prop_of thm
   4.161 +               of Const("==>",_) $ imp $ _ =>
   4.162                     eliminate
   4.163                      (if not(is_all imp)
   4.164 -                     then uq_eliminate (thm,imp,thy)
   4.165 -                     else q_eliminate (thm,imp,thy))
   4.166 +                     then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
   4.167 +                     else q_eliminate (thm, imp, Thm.theory_of_thm thm))
   4.168                              (* Assume that the leading constant is ==,   *)
   4.169                  | _ => thm  (* if it is not a ==>                        *)
   4.170           in SOME(eliminate (rename thm)) end
   4.171 @@ -760,8 +762,8 @@
   4.172            let val dummy = say "restrict_prover:"
   4.173                val cntxt = rev(MetaSimplifier.prems_of_ss ss)
   4.174                val dummy = print_thms "cntxt:" cntxt
   4.175 -              val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   4.176 -                   thy,...} = rep_thm thm
   4.177 +              val thy = Thm.theory_of_thm thm
   4.178 +              val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
   4.179                fun genl tm = let val vlist = subtract (op aconv) globals
   4.180                                             (add_term_frees(tm,[]))
   4.181                              in fold_rev Forall vlist tm
   4.182 @@ -814,7 +816,8 @@
   4.183  
   4.184  fun prove strict (ptm, tac) =
   4.185    let
   4.186 -    val {thy, t, ...} = Thm.rep_cterm ptm;
   4.187 +    val thy = Thm.theory_of_cterm ptm;
   4.188 +    val t = Thm.term_of ptm;
   4.189      val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
   4.190    in
   4.191      if strict then Goal.prove ctxt [] [] t (K tac)
     5.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Apr 10 20:54:18 2008 +0200
     5.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sat Apr 12 17:00:35 2008 +0200
     5.3 @@ -27,8 +27,7 @@
     5.4    in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
     5.5  
     5.6  fun prf_of thm =
     5.7 -  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
     5.8 -  in Reconstruct.reconstruct_proof thy prop prf end;
     5.9 +  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    5.10  
    5.11  fun prf_subst_vars inst =
    5.12    Proofterm.map_proof_terms (subst_vars ([], inst)) I;
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 10 20:54:18 2008 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Apr 12 17:00:35 2008 +0200
     6.3 @@ -359,7 +359,8 @@
     6.4  
     6.5      fun mk_funs_inv thm =
     6.6        let
     6.7 -        val {thy, prop, ...} = rep_thm thm;
     6.8 +        val thy = Thm.theory_of_thm thm;
     6.9 +        val prop = Thm.prop_of thm;
    6.10          val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
    6.11            (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
    6.12          val used = add_term_tfree_names (a, []);
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 10 20:54:18 2008 +0200
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Apr 12 17:00:35 2008 +0200
     7.3 @@ -24,8 +24,10 @@
     7.4  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
     7.5  
     7.6  fun prf_of thm =
     7.7 -  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
     7.8 -  in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
     7.9 +  let
    7.10 +    val thy = Thm.theory_of_thm thm;
    7.11 +    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
    7.12 +  in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
    7.13  
    7.14  fun forall_intr_prf (t, prf) =
    7.15    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     8.1 --- a/src/HOL/Tools/record_package.ML	Thu Apr 10 20:54:18 2008 +0200
     8.2 +++ b/src/HOL/Tools/record_package.ML	Sat Apr 12 17:00:35 2008 +0200
     8.3 @@ -1740,7 +1740,8 @@
     8.4  
     8.5  fun meta_to_obj_all thm =
     8.6    let
     8.7 -    val {thy, prop, ...} = rep_thm thm;
     8.8 +    val thy = Thm.theory_of_thm thm;
     8.9 +    val prop = Thm.prop_of thm;
    8.10      val params = Logic.strip_params prop;
    8.11      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
    8.12      val ct = cterm_of thy
     9.1 --- a/src/HOLCF/Tools/adm_tac.ML	Thu Apr 10 20:54:18 2008 +0200
     9.2 +++ b/src/HOLCF/Tools/adm_tac.ML	Sat Apr 12 17:00:35 2008 +0200
     9.3 @@ -110,8 +110,9 @@
     9.4  (*** instantiation of adm_subst theorem (a bit tricky) ***)
     9.5  
     9.6  fun inst_adm_subst_thm state i params s T subt t paths =
     9.7 -  let val {thy = sign, maxidx, ...} = rep_thm state;
     9.8 -      val j = maxidx+1;
     9.9 +  let
    9.10 +      val sign = Thm.theory_of_thm state;
    9.11 +      val j = Thm.maxidx_of state + 1;
    9.12        val parTs = map snd (rev params);
    9.13        val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
    9.14        val types = valOf o (fst (types_sorts rule));
    10.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 10 20:54:18 2008 +0200
    10.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 12 17:00:35 2008 +0200
    10.3 @@ -564,7 +564,8 @@
    10.4        NONE =>
    10.5          let
    10.6            val (ctxt, (_, thm)) = Proof.get_goal state;
    10.7 -          val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
    10.8 +          val thy = ProofContext.theory_of ctxt;
    10.9 +          val prf = Thm.proof_of thm;
   10.10            val prop = Thm.full_prop_of thm;
   10.11            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
   10.12          in
    11.1 --- a/src/Pure/Proof/extraction.ML	Thu Apr 10 20:54:18 2008 +0200
    11.2 +++ b/src/Pure/Proof/extraction.ML	Sat Apr 12 17:00:35 2008 +0200
    11.3 @@ -711,7 +711,9 @@
    11.4  
    11.5      fun prep_thm (thm, vs) =
    11.6        let
    11.7 -        val {prop, der = (_, prf), thy, ...} = rep_thm thm;
    11.8 +        val thy = Thm.theory_of_thm thm;
    11.9 +        val prop = Thm.prop_of thm;
   11.10 +        val prf = Thm.proof_of thm;
   11.11          val name = Thm.get_name thm;
   11.12          val _ = name <> "" orelse error "extraction: unnamed theorem";
   11.13          val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
    12.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Apr 10 20:54:18 2008 +0200
    12.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Apr 12 17:00:35 2008 +0200
    12.3 @@ -259,8 +259,9 @@
    12.4  
    12.5  fun proof_of full thm =
    12.6    let
    12.7 -    val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
    12.8 +    val thy = Thm.theory_of_thm thm;
    12.9      val prop = Thm.full_prop_of thm;
   12.10 +    val prf = Thm.proof_of thm;
   12.11      val prf' = (case strip_combt (fst (strip_combP prf)) of
   12.12          (PThm (_, prf', prop', _), _) => if prop = prop' then prf' else prf
   12.13        | _ => prf)
    13.1 --- a/src/Pure/codegen.ML	Thu Apr 10 20:54:18 2008 +0200
    13.2 +++ b/src/Pure/codegen.ML	Sat Apr 12 17:00:35 2008 +0200
    13.3 @@ -1074,8 +1074,8 @@
    13.4    Logic.mk_equals (t, eval_term thy t);
    13.5  
    13.6  fun evaluation_conv ct =
    13.7 -  let val {thy, t, ...} = rep_cterm ct
    13.8 -  in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
    13.9 +  let val thy = Thm.theory_of_cterm ct
   13.10 +  in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
   13.11  
   13.12  val _ = Context.>> (Context.map_theory
   13.13    (Theory.add_oracle ("evaluation", evaluation_oracle)));
    14.1 --- a/src/Pure/display.ML	Thu Apr 10 20:54:18 2008 +0200
    14.2 +++ b/src/Pure/display.ML	Sat Apr 12 17:00:35 2008 +0200
    14.3 @@ -109,20 +109,12 @@
    14.4  
    14.5  (* other printing commands *)
    14.6  
    14.7 -fun pretty_ctyp cT =
    14.8 -  let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
    14.9 -
   14.10 -fun string_of_ctyp cT =
   14.11 -  let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
   14.12 -
   14.13 +fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   14.14 +fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   14.15  val print_ctyp = writeln o string_of_ctyp;
   14.16  
   14.17 -fun pretty_cterm ct =
   14.18 -  let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
   14.19 -
   14.20 -fun string_of_cterm ct =
   14.21 -  let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
   14.22 -
   14.23 +fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
   14.24 +fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
   14.25  val print_cterm = writeln o string_of_cterm;
   14.26  
   14.27  
    15.1 --- a/src/Pure/meta_simplifier.ML	Thu Apr 10 20:54:18 2008 +0200
    15.2 +++ b/src/Pure/meta_simplifier.ML	Sat Apr 12 17:00:35 2008 +0200
    15.3 @@ -458,7 +458,8 @@
    15.4  
    15.5  fun decomp_simp thm =
    15.6    let
    15.7 -    val {thy, prop, ...} = Thm.rep_thm thm;
    15.8 +    val thy = Thm.theory_of_thm thm;
    15.9 +    val prop = Thm.prop_of thm;
   15.10      val prems = Logic.strip_imp_prems prop;
   15.11      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
   15.12      val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
   15.13 @@ -833,7 +834,10 @@
   15.14         (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
   15.15    in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
   15.16    handle THM _ =>
   15.17 -    let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
   15.18 +    let
   15.19 +      val thy = Thm.theory_of_thm thm;
   15.20 +      val _ $ _ $ prop0 = Thm.prop_of thm;
   15.21 +    in
   15.22        trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
   15.23        trace_term false (fn () => "Should have proved:") ss thy prop0;
   15.24        NONE
   15.25 @@ -897,7 +901,8 @@
   15.26      val eta_t = term_of eta_t';
   15.27      fun rew {thm, name, lhs, elhs, extra, fo, perm} =
   15.28        let
   15.29 -        val {thy, prop, maxidx, ...} = rep_thm thm;
   15.30 +        val thy = Thm.theory_of_thm thm;
   15.31 +        val {prop, maxidx, ...} = rep_thm thm;
   15.32          val (rthm, elhs') =
   15.33            if maxt = ~1 orelse not extra then (thm, elhs)
   15.34            else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
   15.35 @@ -1233,8 +1238,9 @@
   15.36  
   15.37  fun rewrite_cterm mode prover raw_ss raw_ct =
   15.38    let
   15.39 +    val thy = Thm.theory_of_cterm raw_ct;
   15.40      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
   15.41 -    val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
   15.42 +    val {t, maxidx, ...} = Thm.rep_cterm ct;
   15.43      val ss = inc_simp_depth (activate_context thy raw_ss);
   15.44      val depth = simp_depth ss;
   15.45      val _ =
    16.1 --- a/src/Pure/old_goals.ML	Thu Apr 10 20:54:18 2008 +0200
    16.2 +++ b/src/Pure/old_goals.ML	Sat Apr 12 17:00:35 2008 +0200
    16.3 @@ -151,7 +151,8 @@
    16.4  fun prepare_proof atomic rths chorn =
    16.5    let
    16.6        val _ = legacy_feature "Old goal command";
    16.7 -      val {thy, t=horn,...} = rep_cterm chorn;
    16.8 +      val thy = Thm.theory_of_cterm chorn;
    16.9 +      val horn = Thm.term_of chorn;
   16.10        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
   16.11        val (As, B) = Logic.strip_horn horn;
   16.12        val atoms = atomic andalso
   16.13 @@ -170,7 +171,8 @@
   16.14              val ngoals = nprems_of state
   16.15              val ath = implies_intr_list cAs state
   16.16              val th = Goal.conclude ath
   16.17 -            val {hyps,prop,thy=thy',...} = rep_thm th
   16.18 +            val thy' = Thm.theory_of_thm th
   16.19 +            val {hyps, prop, ...} = Thm.rep_thm th
   16.20              val final_th = standard th
   16.21          in  if not check then final_th
   16.22              else if not (eq_thy(thy,thy')) then !result_error_fn state
   16.23 @@ -229,7 +231,7 @@
   16.24                 SOME(st,_) => st
   16.25               | _ => error ("prove_goal: tactic failed"))
   16.26    in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end
   16.27 -  handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
   16.28 +  handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
   16.29                 writeln ("The exception above was raised for\n" ^
   16.30                        Display.string_of_cterm chorn); raise e);
   16.31  
    17.1 --- a/src/Pure/pure_thy.ML	Thu Apr 10 20:54:18 2008 +0200
    17.2 +++ b/src/Pure/pure_thy.ML	Sat Apr 12 17:00:35 2008 +0200
    17.3 @@ -337,7 +337,8 @@
    17.4  
    17.5  fun forall_elim_vars_aux strip_vars i th =
    17.6    let
    17.7 -    val {thy, tpairs, prop, ...} = Thm.rep_thm th;
    17.8 +    val thy = Thm.theory_of_thm th;
    17.9 +    val {tpairs, prop, ...} = Thm.rep_thm th;
   17.10      val add_used = Term.fold_aterms
   17.11        (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I);
   17.12      val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
    18.1 --- a/src/Pure/tactic.ML	Thu Apr 10 20:54:18 2008 +0200
    18.2 +++ b/src/Pure/tactic.ML	Sat Apr 12 17:00:35 2008 +0200
    18.3 @@ -263,15 +263,19 @@
    18.4      i.e. Tinsts is not applied to insts.
    18.5  *)
    18.6  fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
    18.7 -let val {maxidx,thy,...} = rep_thm st
    18.8 +let
    18.9 +    val thy = Thm.theory_of_thm st
   18.10 +    val cert = Thm.cterm_of thy
   18.11 +    val certT = Thm.ctyp_of thy
   18.12 +    val maxidx = Thm.maxidx_of st
   18.13      val paramTs = map #2 (params_of_state i st)
   18.14 -    and inc = maxidx+1
   18.15 +    val inc = maxidx+1
   18.16      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
   18.17      (*lift only Var, not term, which must be lifted already*)
   18.18 -    fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
   18.19 +    fun liftpair (v,t) = (cert (liftvar v), cert t)
   18.20      fun liftTpair (((a, i), S), T) =
   18.21 -      (ctyp_of thy (TVar ((a, i + inc), S)),
   18.22 -       ctyp_of thy (Logic.incr_tvar inc T))
   18.23 +      (certT (TVar ((a, i + inc), S)),
   18.24 +       certT (Logic.incr_tvar inc T))
   18.25  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
   18.26                       (Thm.lift_rule (Thm.cprem_of st i) rule)
   18.27  end;
    19.1 --- a/src/Pure/tctical.ML	Thu Apr 10 20:54:18 2008 +0200
    19.2 +++ b/src/Pure/tctical.ML	Sat Apr 12 17:00:35 2008 +0200
    19.3 @@ -425,8 +425,8 @@
    19.4  
    19.5  fun metahyps_aux_tac tacf (prem,gno) state =
    19.6    let val (insts,params,hyps,concl) = metahyps_split_prem prem
    19.7 -      val {thy = sign,maxidx,...} = rep_thm state
    19.8 -      val cterm = cterm_of sign
    19.9 +      val maxidx = Thm.maxidx_of state
   19.10 +      val cterm = Thm.cterm_of (Thm.theory_of_thm state)
   19.11        val chyps = map cterm hyps
   19.12        val hypths = map assume chyps
   19.13        val subprems = map (forall_elim_vars 0) hypths
    20.1 --- a/src/Tools/Compute_Oracle/compute.ML	Thu Apr 10 20:54:18 2008 +0200
    20.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Sat Apr 12 17:00:35 2008 +0200
    20.3 @@ -43,7 +43,7 @@
    20.4  
    20.5  open Report;
    20.6  
    20.7 -datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML	 
    20.8 +datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML      
    20.9  
   20.10  (* Terms are mapped to integer codes *)
   20.11  structure Encode :> 
   20.12 @@ -52,10 +52,10 @@
   20.13      val empty : encoding
   20.14      val insert : term -> encoding -> int * encoding
   20.15      val lookup_code : term -> encoding -> int option
   20.16 -    val lookup_term : int -> encoding -> term option					
   20.17 +    val lookup_term : int -> encoding -> term option                                    
   20.18      val remove_code : int -> encoding -> encoding
   20.19      val remove_term : term -> encoding -> encoding
   20.20 -    val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a  						       
   20.21 +    val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a                                                      
   20.22  end 
   20.23  = 
   20.24  struct
   20.25 @@ -66,7 +66,7 @@
   20.26  
   20.27  fun insert t (e as (count, term2int, int2term)) = 
   20.28      (case Termtab.lookup term2int t of
   20.29 -	 NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
   20.30 +         NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
   20.31         | SOME code => (code, e))
   20.32  
   20.33  fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
   20.34 @@ -88,29 +88,29 @@
   20.35  
   20.36  local
   20.37      fun make_constant t ty encoding = 
   20.38 -	let 
   20.39 -	    val (code, encoding) = Encode.insert t encoding 
   20.40 -	in 
   20.41 -	    (encoding, AbstractMachine.Const code)
   20.42 -	end
   20.43 +        let 
   20.44 +            val (code, encoding) = Encode.insert t encoding 
   20.45 +        in 
   20.46 +            (encoding, AbstractMachine.Const code)
   20.47 +        end
   20.48  in
   20.49  
   20.50  fun remove_types encoding t =
   20.51      case t of 
   20.52 -	Var (_, ty) => make_constant t ty encoding
   20.53 +        Var (_, ty) => make_constant t ty encoding
   20.54        | Free (_, ty) => make_constant t ty encoding
   20.55        | Const (_, ty) => make_constant t ty encoding
   20.56        | Abs (_, ty, t') => 
   20.57 -	let val (encoding, t'') = remove_types encoding t' in
   20.58 -	    (encoding, AbstractMachine.Abs t'')
   20.59 -	end
   20.60 +        let val (encoding, t'') = remove_types encoding t' in
   20.61 +            (encoding, AbstractMachine.Abs t'')
   20.62 +        end
   20.63        | a $ b => 
   20.64 -	let
   20.65 -	    val (encoding, a) = remove_types encoding a
   20.66 -	    val (encoding, b) = remove_types encoding b
   20.67 -	in
   20.68 -	    (encoding, AbstractMachine.App (a,b))
   20.69 -	end
   20.70 +        let
   20.71 +            val (encoding, a) = remove_types encoding a
   20.72 +            val (encoding, b) = remove_types encoding b
   20.73 +        in
   20.74 +            (encoding, AbstractMachine.App (a,b))
   20.75 +        end
   20.76        | Bound b => (encoding, AbstractMachine.Var b)
   20.77  end
   20.78      
   20.79 @@ -123,23 +123,23 @@
   20.80  fun infer_types naming encoding =
   20.81      let
   20.82          fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
   20.83 -	  | infer_types _ bounds _ (AbstractMachine.Const code) = 
   20.84 -	    let
   20.85 -		val c = the (Encode.lookup_term code encoding)
   20.86 -	    in
   20.87 -		(c, type_of c)
   20.88 -	    end
   20.89 -	  | infer_types level bounds _ (AbstractMachine.App (a, b)) = 
   20.90 -	    let
   20.91 -		val (a, aty) = infer_types level bounds NONE a
   20.92 -		val (adom, arange) =
   20.93 +          | infer_types _ bounds _ (AbstractMachine.Const code) = 
   20.94 +            let
   20.95 +                val c = the (Encode.lookup_term code encoding)
   20.96 +            in
   20.97 +                (c, type_of c)
   20.98 +            end
   20.99 +          | infer_types level bounds _ (AbstractMachine.App (a, b)) = 
  20.100 +            let
  20.101 +                val (a, aty) = infer_types level bounds NONE a
  20.102 +                val (adom, arange) =
  20.103                      case aty of
  20.104                          Type ("fun", [dom, range]) => (dom, range)
  20.105                        | _ => sys_error "infer_types: function type expected"
  20.106                  val (b, bty) = infer_types level bounds (SOME adom) b
  20.107 -	    in
  20.108 -		(a $ b, arange)
  20.109 -	    end
  20.110 +            in
  20.111 +                (a $ b, arange)
  20.112 +            end
  20.113            | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
  20.114              let
  20.115                  val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
  20.116 @@ -160,7 +160,7 @@
  20.117  end
  20.118  
  20.119  datatype prog = 
  20.120 -	 ProgBarras of AM_Interpreter.program 
  20.121 +         ProgBarras of AM_Interpreter.program 
  20.122         | ProgBarrasC of AM_Compiler.program
  20.123         | ProgHaskell of AM_GHC.program
  20.124         | ProgSML of AM_SML.program
  20.125 @@ -198,26 +198,26 @@
  20.126  
  20.127  fun thm2cthm th = 
  20.128      let
  20.129 -	val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
  20.130 -	val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
  20.131 +        val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
  20.132 +        val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
  20.133      in
  20.134 -	ComputeThm (hyps, shyps, prop)
  20.135 +        ComputeThm (hyps, shyps, prop)
  20.136      end
  20.137  
  20.138  fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
  20.139      let
  20.140 -	fun transfer (x:thm) = Thm.transfer thy x
  20.141 -	val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
  20.142 +        fun transfer (x:thm) = Thm.transfer thy x
  20.143 +        val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
  20.144  
  20.145          fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
  20.146 -	    raise (Make "no lambda abstractions allowed in pattern")
  20.147 -	  | make_pattern encoding n vars (var as AbstractMachine.Var _) =
  20.148 -	    raise (Make "no bound variables allowed in pattern")
  20.149 -	  | make_pattern encoding n vars (AbstractMachine.Const code) =
  20.150 -	    (case the (Encode.lookup_term code encoding) of
  20.151 -		 Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
  20.152 -			   handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
  20.153 -	       | _ => (n, vars, AbstractMachine.PConst (code, [])))
  20.154 +            raise (Make "no lambda abstractions allowed in pattern")
  20.155 +          | make_pattern encoding n vars (var as AbstractMachine.Var _) =
  20.156 +            raise (Make "no bound variables allowed in pattern")
  20.157 +          | make_pattern encoding n vars (AbstractMachine.Const code) =
  20.158 +            (case the (Encode.lookup_term code encoding) of
  20.159 +                 Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
  20.160 +                           handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
  20.161 +               | _ => (n, vars, AbstractMachine.PConst (code, [])))
  20.162            | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
  20.163              let
  20.164                  val (n, vars, pa) = make_pattern encoding n vars a
  20.165 @@ -232,26 +232,26 @@
  20.166  
  20.167          fun thm2rule (encoding, hyptable, shyptable) th =
  20.168              let
  20.169 -		val (ComputeThm (hyps, shyps, prop)) = th
  20.170 -		val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
  20.171 -		val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
  20.172 -		val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
  20.173 +                val (ComputeThm (hyps, shyps, prop)) = th
  20.174 +                val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
  20.175 +                val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
  20.176 +                val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
  20.177                  val (a, b) = Logic.dest_equals prop
  20.178                    handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
  20.179 -		val a = Envir.eta_contract a
  20.180 -		val b = Envir.eta_contract b
  20.181 -		val prems = map Envir.eta_contract prems
  20.182 +                val a = Envir.eta_contract a
  20.183 +                val b = Envir.eta_contract b
  20.184 +                val prems = map Envir.eta_contract prems
  20.185  
  20.186                  val (encoding, left) = remove_types encoding a     
  20.187 -		val (encoding, right) = remove_types encoding b  
  20.188 +                val (encoding, right) = remove_types encoding b  
  20.189                  fun remove_types_of_guard encoding g = 
  20.190 -		    (let
  20.191 -			 val (t1, t2) = Logic.dest_equals g 
  20.192 -			 val (encoding, t1) = remove_types encoding t1
  20.193 -			 val (encoding, t2) = remove_types encoding t2
  20.194 -		     in
  20.195 -			 (encoding, AbstractMachine.Guard (t1, t2))
  20.196 -		     end handle TERM _ => raise (Make "guards must be meta-level equations"))
  20.197 +                    (let
  20.198 +                         val (t1, t2) = Logic.dest_equals g 
  20.199 +                         val (encoding, t1) = remove_types encoding t1
  20.200 +                         val (encoding, t2) = remove_types encoding t2
  20.201 +                     in
  20.202 +                         (encoding, AbstractMachine.Guard (t1, t2))
  20.203 +                     end handle TERM _ => raise (Make "guards must be meta-level equations"))
  20.204                  val (encoding, prems) = fold_rev (fn p => fn (encoding, ps) => let val (e, p) = remove_types_of_guard encoding p in (e, p::ps) end) prems (encoding, [])
  20.205  
  20.206                  (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
  20.207 @@ -263,24 +263,24 @@
  20.208                               AbstractMachine.PVar =>
  20.209                               raise (Make "patterns may not start with a variable")
  20.210                           (*  | AbstractMachine.PConst (_, []) => 
  20.211 -			     (print th; raise (Make "no parameter rewrite found"))*)
  20.212 -			   | _ => ())
  20.213 +                             (print th; raise (Make "no parameter rewrite found"))*)
  20.214 +                           | _ => ())
  20.215  
  20.216                  (* finally, provide a function for renaming the
  20.217                     pattern bound variables on the right hand side *)
  20.218  
  20.219                  fun rename level vars (var as AbstractMachine.Var _) = var
  20.220 -		  | rename level vars (c as AbstractMachine.Const code) =
  20.221 -		    (case Inttab.lookup vars code of 
  20.222 -			 NONE => c 
  20.223 -		       | SOME n => AbstractMachine.Var (vcount-n-1+level))
  20.224 +                  | rename level vars (c as AbstractMachine.Const code) =
  20.225 +                    (case Inttab.lookup vars code of 
  20.226 +                         NONE => c 
  20.227 +                       | SOME n => AbstractMachine.Var (vcount-n-1+level))
  20.228                    | rename level vars (AbstractMachine.App (a, b)) =
  20.229                      AbstractMachine.App (rename level vars a, rename level vars b)
  20.230                    | rename level vars (AbstractMachine.Abs m) =
  20.231                      AbstractMachine.Abs (rename (level+1) vars m)
  20.232 -		    
  20.233 -		fun rename_guard (AbstractMachine.Guard (a,b)) = 
  20.234 -		    AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
  20.235 +                    
  20.236 +                fun rename_guard (AbstractMachine.Guard (a,b)) = 
  20.237 +                    AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
  20.238              in
  20.239                  ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
  20.240              end
  20.241 @@ -293,35 +293,35 @@
  20.242            ths ((encoding, Termtab.empty, Sorttab.empty), [])
  20.243  
  20.244          fun make_cache_pattern t (encoding, cache_patterns) =
  20.245 -	    let
  20.246 -		val (encoding, a) = remove_types encoding t
  20.247 -		val (_,_,p) = make_pattern encoding 0 Inttab.empty a
  20.248 -	    in
  20.249 -		(encoding, p::cache_patterns)
  20.250 -	    end
  20.251 -	
  20.252 -	val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
  20.253 +            let
  20.254 +                val (encoding, a) = remove_types encoding t
  20.255 +                val (_,_,p) = make_pattern encoding 0 Inttab.empty a
  20.256 +            in
  20.257 +                (encoding, p::cache_patterns)
  20.258 +            end
  20.259 +        
  20.260 +        val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
  20.261  
  20.262 -	fun arity (Type ("fun", [a,b])) = 1 + arity b
  20.263 -	  | arity _ = 0
  20.264 +        fun arity (Type ("fun", [a,b])) = 1 + arity b
  20.265 +          | arity _ = 0
  20.266  
  20.267 -	fun make_arity (Const (s, _), i) tab = 
  20.268 -	    (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
  20.269 -	  | make_arity _ tab = tab
  20.270 +        fun make_arity (Const (s, _), i) tab = 
  20.271 +            (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
  20.272 +          | make_arity _ tab = tab
  20.273  
  20.274 -	val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
  20.275 -	fun const_arity x = Inttab.lookup const_arity_tab x 
  20.276 +        val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
  20.277 +        fun const_arity x = Inttab.lookup const_arity_tab x 
  20.278  
  20.279          val prog = 
  20.280 -	    case machine of 
  20.281 -		BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
  20.282 -	      | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
  20.283 -	      | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
  20.284 -	      | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
  20.285 +            case machine of 
  20.286 +                BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
  20.287 +              | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
  20.288 +              | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
  20.289 +              | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
  20.290  
  20.291          fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
  20.292  
  20.293 -	val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
  20.294 +        val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
  20.295  
  20.296      in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
  20.297  
  20.298 @@ -331,32 +331,32 @@
  20.299  
  20.300  fun update_with_cache computer cache_patterns raw_thms =
  20.301      let 
  20.302 -	val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) 
  20.303 -			      (encoding_of computer) cache_patterns raw_thms
  20.304 -	val _ = (ref_of computer) := SOME c	
  20.305 +        val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) 
  20.306 +                              (encoding_of computer) cache_patterns raw_thms
  20.307 +        val _ = (ref_of computer) := SOME c     
  20.308      in
  20.309 -	()
  20.310 +        ()
  20.311      end
  20.312  
  20.313  fun update computer raw_thms = update_with_cache computer [] raw_thms
  20.314  
  20.315  fun discard computer =
  20.316      let
  20.317 -	val _ = 
  20.318 -	    case prog_of computer of
  20.319 -		ProgBarras p => AM_Interpreter.discard p
  20.320 -	      | ProgBarrasC p => AM_Compiler.discard p
  20.321 -	      | ProgHaskell p => AM_GHC.discard p
  20.322 -	      | ProgSML p => AM_SML.discard p
  20.323 -	val _ = (ref_of computer) := NONE
  20.324 +        val _ = 
  20.325 +            case prog_of computer of
  20.326 +                ProgBarras p => AM_Interpreter.discard p
  20.327 +              | ProgBarrasC p => AM_Compiler.discard p
  20.328 +              | ProgHaskell p => AM_GHC.discard p
  20.329 +              | ProgSML p => AM_SML.discard p
  20.330 +        val _ = (ref_of computer) := NONE
  20.331      in
  20.332 -	()
  20.333 +        ()
  20.334      end 
  20.335 -					      
  20.336 +                                              
  20.337  fun runprog (ProgBarras p) = AM_Interpreter.run p
  20.338    | runprog (ProgBarrasC p) = AM_Compiler.run p
  20.339    | runprog (ProgHaskell p) = AM_GHC.run p
  20.340 -  | runprog (ProgSML p) = AM_SML.run p	  
  20.341 +  | runprog (ProgSML p) = AM_SML.run p    
  20.342  
  20.343  (* ------------------------------------------------------------------------------------- *)
  20.344  (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
  20.345 @@ -377,15 +377,15 @@
  20.346  
  20.347  fun export_oracle (thy, ExportThm (hyps, shyps, prop)) =
  20.348      let
  20.349 -	val shyptab = add_shyps shyps Sorttab.empty
  20.350 -	fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
  20.351 -	fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
  20.352 -	fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
  20.353 -	val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
  20.354 -	val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
  20.355 -	val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
  20.356 +        val shyptab = add_shyps shyps Sorttab.empty
  20.357 +        fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
  20.358 +        fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
  20.359 +        fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
  20.360 +        val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
  20.361 +        val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
  20.362 +        val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
  20.363      in
  20.364 -	fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
  20.365 +        fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
  20.366      end
  20.367    | export_oracle _ = raise Match
  20.368  
  20.369 @@ -393,24 +393,25 @@
  20.370  
  20.371  fun export_thm thy hyps shyps prop =
  20.372      let
  20.373 -	val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
  20.374 -	val hyps = map (fn h => assume (cterm_of thy h)) hyps
  20.375 +        val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
  20.376 +        val hyps = map (fn h => assume (cterm_of thy h)) hyps
  20.377      in
  20.378 -	fold (fn h => fn p => implies_elim p h) hyps th 
  20.379 +        fold (fn h => fn p => implies_elim p h) hyps th 
  20.380      end
  20.381 -	
  20.382 +        
  20.383  (* --------- Rewrite ----------- *)
  20.384  
  20.385  fun rewrite computer ct =
  20.386      let
  20.387 -	val {t=t',T=ty,thy=thy,...} = rep_cterm ct
  20.388 -	val _ = Theory.assert_super (theory_of computer) thy
  20.389 -	val naming = naming_of computer
  20.390 +        val thy = Thm.theory_of_cterm ct
  20.391 +        val {t=t',T=ty,...} = rep_cterm ct
  20.392 +        val _ = Theory.assert_super (theory_of computer) thy
  20.393 +        val naming = naming_of computer
  20.394          val (encoding, t) = remove_types (encoding_of computer) t'
  20.395 -	(*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*)
  20.396 +        (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*)
  20.397          val t = runprog (prog_of computer) t
  20.398          val t = infer_types naming encoding ty t
  20.399 -	val eq = Logic.mk_equals (t', t)
  20.400 +        val eq = Logic.mk_equals (t', t)
  20.401      in
  20.402          export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq
  20.403      end
  20.404 @@ -418,7 +419,7 @@
  20.405  (* --------- Simplify ------------ *)
  20.406  
  20.407  datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int 
  20.408 -	      | Prem of AbstractMachine.term
  20.409 +              | Prem of AbstractMachine.term
  20.410  datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table  
  20.411                 * prem list * AbstractMachine.term * term list * sort list
  20.412  
  20.413 @@ -439,46 +440,46 @@
  20.414        | collect_vars (Const _) tab = tab
  20.415        | collect_vars (Free _) tab = tab
  20.416        | collect_vars (Var ((s, i), ty)) tab = 
  20.417 -	    if List.find (fn x => x=s) vars = NONE then 
  20.418 -		tab
  20.419 -	    else		
  20.420 -		(case Symtab.lookup tab s of
  20.421 -		     SOME ((s',i'),ty') => 
  20.422 -	             if s' <> s orelse i' <> i orelse ty <> ty' then 
  20.423 -			 raise Compute ("make_theorem: variable name '"^s^"' is not unique")
  20.424 -		     else 
  20.425 -			 tab
  20.426 -		   | NONE => Symtab.update (s, ((s, i), ty)) tab)
  20.427 +            if List.find (fn x => x=s) vars = NONE then 
  20.428 +                tab
  20.429 +            else                
  20.430 +                (case Symtab.lookup tab s of
  20.431 +                     SOME ((s',i'),ty') => 
  20.432 +                     if s' <> s orelse i' <> i orelse ty <> ty' then 
  20.433 +                         raise Compute ("make_theorem: variable name '"^s^"' is not unique")
  20.434 +                     else 
  20.435 +                         tab
  20.436 +                   | NONE => Symtab.update (s, ((s, i), ty)) tab)
  20.437      val vartab = collect_vars prop Symtab.empty 
  20.438      fun encodevar (s, t as (_, ty)) (encoding, tab) = 
  20.439 -	let
  20.440 -	    val (x, encoding) = Encode.insert (Var t) encoding
  20.441 -	in
  20.442 -	    (encoding, Symtab.update (s, (x, ty)) tab)
  20.443 -	end
  20.444 -    val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)  					 	       
  20.445 +        let
  20.446 +            val (x, encoding) = Encode.insert (Var t) encoding
  20.447 +        in
  20.448 +            (encoding, Symtab.update (s, (x, ty)) tab)
  20.449 +        end
  20.450 +    val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)                                                     
  20.451      val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab))
  20.452  
  20.453      (* make the premises and the conclusion *)
  20.454      fun mk_prem encoding t = 
  20.455 -	(let
  20.456 -	     val (a, b) = Logic.dest_equals t
  20.457 -	     val ty = type_of a
  20.458 -	     val (encoding, a) = remove_types encoding a
  20.459 -	     val (encoding, b) = remove_types encoding b
  20.460 -	     val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding 
  20.461 -	 in
  20.462 -	     (encoding, EqPrem (a, b, ty, eq))
  20.463 -	 end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
  20.464 +        (let
  20.465 +             val (a, b) = Logic.dest_equals t
  20.466 +             val ty = type_of a
  20.467 +             val (encoding, a) = remove_types encoding a
  20.468 +             val (encoding, b) = remove_types encoding b
  20.469 +             val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding 
  20.470 +         in
  20.471 +             (encoding, EqPrem (a, b, ty, eq))
  20.472 +         end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
  20.473      val (encoding, prems) = 
  20.474 -	(fold_rev (fn t => fn (encoding, l) => 
  20.475 -	    case mk_prem encoding t  of 
  20.476 +        (fold_rev (fn t => fn (encoding, l) => 
  20.477 +            case mk_prem encoding t  of 
  20.478                  (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, []))
  20.479      val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop)
  20.480      val _ = set_encoding computer encoding
  20.481  in
  20.482      Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, 
  20.483 -	     prems, concl, hyps, shyps)
  20.484 +             prems, concl, hyps, shyps)
  20.485  end
  20.486      
  20.487  fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy
  20.488 @@ -498,7 +499,7 @@
  20.489  
  20.490  fun check_compatible computer th s = 
  20.491      if stamp_of computer <> stamp_of_theorem th then
  20.492 -	raise Compute (s^": computer and theorem are incompatible")
  20.493 +        raise Compute (s^": computer and theorem are incompatible")
  20.494      else ()
  20.495  
  20.496  fun instantiate computer insts th =
  20.497 @@ -511,49 +512,49 @@
  20.498  
  20.499      fun rewrite computer t =
  20.500      let  
  20.501 -	val naming = naming_of computer
  20.502 +        val naming = naming_of computer
  20.503          val (encoding, t) = remove_types (encoding_of computer) t
  20.504          val t = runprog (prog_of computer) t
  20.505 -	val _ = set_encoding computer encoding
  20.506 +        val _ = set_encoding computer encoding
  20.507      in
  20.508          t
  20.509      end
  20.510  
  20.511      fun assert_varfree vs t = 
  20.512 -	if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then
  20.513 -	    ()
  20.514 -	else
  20.515 -	    raise Compute "instantiate: assert_varfree failed"
  20.516 +        if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then
  20.517 +            ()
  20.518 +        else
  20.519 +            raise Compute "instantiate: assert_varfree failed"
  20.520  
  20.521      fun assert_closed t =
  20.522 -	if AbstractMachine.closed t then
  20.523 -	    ()
  20.524 -	else 
  20.525 -	    raise Compute "instantiate: not a closed term"
  20.526 +        if AbstractMachine.closed t then
  20.527 +            ()
  20.528 +        else 
  20.529 +            raise Compute "instantiate: not a closed term"
  20.530  
  20.531      fun compute_inst (s, ct) vs =
  20.532 -	let
  20.533 -	    val _ = Theory.assert_super (theory_of_cterm ct) thy
  20.534 -	    val ty = typ_of (ctyp_of_term ct) 
  20.535 -	in	    
  20.536 -	    (case Symtab.lookup vartab s of 
  20.537 -		 NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
  20.538 -	       | SOME (x, ty') => 
  20.539 -		 (case Inttab.lookup vs x of 
  20.540 -		      SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated")
  20.541 -		    | SOME NONE => 
  20.542 -		      if ty <> ty' then 
  20.543 -			  raise Compute ("instantiate: wrong type for variable '"^s^"'")
  20.544 -		      else
  20.545 -			  let
  20.546 -			      val t = rewrite computer (term_of ct)
  20.547 -			      val _ = assert_varfree vs t 
  20.548 -			      val _ = assert_closed t
  20.549 -			  in
  20.550 -			      Inttab.update (x, SOME t) vs
  20.551 -			  end
  20.552 -		    | NONE => raise Compute "instantiate: internal error"))
  20.553 -	end
  20.554 +        let
  20.555 +            val _ = Theory.assert_super (theory_of_cterm ct) thy
  20.556 +            val ty = typ_of (ctyp_of_term ct) 
  20.557 +        in          
  20.558 +            (case Symtab.lookup vartab s of 
  20.559 +                 NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
  20.560 +               | SOME (x, ty') => 
  20.561 +                 (case Inttab.lookup vs x of 
  20.562 +                      SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated")
  20.563 +                    | SOME NONE => 
  20.564 +                      if ty <> ty' then 
  20.565 +                          raise Compute ("instantiate: wrong type for variable '"^s^"'")
  20.566 +                      else
  20.567 +                          let
  20.568 +                              val t = rewrite computer (term_of ct)
  20.569 +                              val _ = assert_varfree vs t 
  20.570 +                              val _ = assert_closed t
  20.571 +                          in
  20.572 +                              Inttab.update (x, SOME t) vs
  20.573 +                          end
  20.574 +                    | NONE => raise Compute "instantiate: internal error"))
  20.575 +        end
  20.576  
  20.577      val vs = fold compute_inst insts (varsubst_of_theorem th)
  20.578  in
  20.579 @@ -561,39 +562,39 @@
  20.580  end
  20.581  
  20.582  fun match_aterms subst =
  20.583 -    let	
  20.584 -	exception no_match
  20.585 -	open AbstractMachine
  20.586 -	fun match subst (b as (Const c)) a = 
  20.587 -	    if a = b then subst
  20.588 -	    else 
  20.589 -		(case Inttab.lookup subst c of 
  20.590 -		     SOME (SOME a') => if a=a' then subst else raise no_match
  20.591 -		   | SOME NONE => if AbstractMachine.closed a then 
  20.592 -				      Inttab.update (c, SOME a) subst 
  20.593 -				  else raise no_match
  20.594 -		   | NONE => raise no_match)
  20.595 -	  | match subst (b as (Var _)) a = if a=b then subst else raise no_match
  20.596 -	  | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v'
  20.597 -	  | match subst (Abs u) (Abs u') = match subst u u'
  20.598 -	  | match subst _ _ = raise no_match
  20.599 +    let 
  20.600 +        exception no_match
  20.601 +        open AbstractMachine
  20.602 +        fun match subst (b as (Const c)) a = 
  20.603 +            if a = b then subst
  20.604 +            else 
  20.605 +                (case Inttab.lookup subst c of 
  20.606 +                     SOME (SOME a') => if a=a' then subst else raise no_match
  20.607 +                   | SOME NONE => if AbstractMachine.closed a then 
  20.608 +                                      Inttab.update (c, SOME a) subst 
  20.609 +                                  else raise no_match
  20.610 +                   | NONE => raise no_match)
  20.611 +          | match subst (b as (Var _)) a = if a=b then subst else raise no_match
  20.612 +          | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v'
  20.613 +          | match subst (Abs u) (Abs u') = match subst u u'
  20.614 +          | match subst _ _ = raise no_match
  20.615      in
  20.616 -	fn b => fn a => (SOME (match subst b a) handle no_match => NONE)
  20.617 +        fn b => fn a => (SOME (match subst b a) handle no_match => NONE)
  20.618      end
  20.619  
  20.620  fun apply_subst vars_allowed subst =
  20.621      let
  20.622 -	open AbstractMachine
  20.623 -	fun app (t as (Const c)) = 
  20.624 -	    (case Inttab.lookup subst c of 
  20.625 -		 NONE => t 
  20.626 -	       | SOME (SOME t) => Computed t
  20.627 -	       | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed")
  20.628 -	  | app (t as (Var _)) = t
  20.629 -	  | app (App (u, v)) = App (app u, app v)
  20.630 -	  | app (Abs m) = Abs (app m)
  20.631 +        open AbstractMachine
  20.632 +        fun app (t as (Const c)) = 
  20.633 +            (case Inttab.lookup subst c of 
  20.634 +                 NONE => t 
  20.635 +               | SOME (SOME t) => Computed t
  20.636 +               | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed")
  20.637 +          | app (t as (Var _)) = t
  20.638 +          | app (App (u, v)) = App (app u, app v)
  20.639 +          | app (Abs m) = Abs (app m)
  20.640      in
  20.641 -	app
  20.642 +        app
  20.643      end
  20.644  
  20.645  fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1)
  20.646 @@ -604,27 +605,27 @@
  20.647      val prems = prems_of_theorem th
  20.648      val varsubst = varsubst_of_theorem th
  20.649      fun run vars_allowed t = 
  20.650 -	runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
  20.651 +        runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
  20.652  in
  20.653      case List.nth (prems, prem_no) of
  20.654 -	Prem _ => raise Compute "evaluate_prem: no equality premise"
  20.655 -      | EqPrem (a, b, ty, _) => 	
  20.656 -	let
  20.657 -	    val a' = run false a
  20.658 -	    val b' = run true b
  20.659 -	in
  20.660 -	    case match_aterms varsubst b' a' of
  20.661 -		NONE => 
  20.662 -		let
  20.663 -		    fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
  20.664 -		    val left = "computed left side: "^(mk a')
  20.665 -		    val right = "computed right side: "^(mk b')
  20.666 -		in
  20.667 -		    raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")
  20.668 -		end
  20.669 -	      | SOME varsubst => 
  20.670 -		update_prems (splicein prem_no [] prems) (update_varsubst varsubst th)
  20.671 -	end
  20.672 +        Prem _ => raise Compute "evaluate_prem: no equality premise"
  20.673 +      | EqPrem (a, b, ty, _) =>         
  20.674 +        let
  20.675 +            val a' = run false a
  20.676 +            val b' = run true b
  20.677 +        in
  20.678 +            case match_aterms varsubst b' a' of
  20.679 +                NONE => 
  20.680 +                let
  20.681 +                    fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
  20.682 +                    val left = "computed left side: "^(mk a')
  20.683 +                    val right = "computed right side: "^(mk b')
  20.684 +                in
  20.685 +                    raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")
  20.686 +                end
  20.687 +              | SOME varsubst => 
  20.688 +                update_prems (splicein prem_no [] prems) (update_varsubst varsubst th)
  20.689 +        end
  20.690  end
  20.691  
  20.692  fun prem2term (Prem t) = t
  20.693 @@ -635,33 +636,33 @@
  20.694  let
  20.695      val _ = check_compatible computer th
  20.696      val thy = 
  20.697 -	let
  20.698 -	    val thy1 = theory_of_theorem th
  20.699 -	    val thy2 = theory_of_thm th'
  20.700 -	in
  20.701 -	    if Context.subthy (thy1, thy2) then thy2 
  20.702 -	    else if Context.subthy (thy2, thy1) then thy1 else
  20.703 -	    raise Compute "modus_ponens: theorems are not compatible with each other"
  20.704 -	end 
  20.705 +        let
  20.706 +            val thy1 = theory_of_theorem th
  20.707 +            val thy2 = theory_of_thm th'
  20.708 +        in
  20.709 +            if Context.subthy (thy1, thy2) then thy2 
  20.710 +            else if Context.subthy (thy2, thy1) then thy1 else
  20.711 +            raise Compute "modus_ponens: theorems are not compatible with each other"
  20.712 +        end 
  20.713      val th' = make_theorem computer th' []
  20.714      val varsubst = varsubst_of_theorem th
  20.715      fun run vars_allowed t =
  20.716 -	runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
  20.717 +        runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
  20.718      val prems = prems_of_theorem th
  20.719      val prem = run true (prem2term (List.nth (prems, prem_no)))
  20.720      val concl = run false (concl_of_theorem th')    
  20.721  in
  20.722      case match_aterms varsubst prem concl of
  20.723 -	NONE => raise Compute "modus_ponens: conclusion does not match premise"
  20.724 +        NONE => raise Compute "modus_ponens: conclusion does not match premise"
  20.725        | SOME varsubst =>
  20.726 -	let
  20.727 -	    val th = update_varsubst varsubst th
  20.728 -	    val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th
  20.729 -	    val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th
  20.730 -	    val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
  20.731 -	in
  20.732 -	    update_theory thy th
  20.733 -	end
  20.734 +        let
  20.735 +            val th = update_varsubst varsubst th
  20.736 +            val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th
  20.737 +            val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th
  20.738 +            val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
  20.739 +        in
  20.740 +            update_theory thy th
  20.741 +        end
  20.742  end
  20.743                       
  20.744  fun simplify computer th =
    21.1 --- a/src/Tools/induct.ML	Thu Apr 10 20:54:18 2008 +0200
    21.2 +++ b/src/Tools/induct.ML	Sat Apr 12 17:00:35 2008 +0200
    21.3 @@ -280,10 +280,11 @@
    21.4      fun prep_var (x, SOME t) =
    21.5            let
    21.6              val cx = cert x;
    21.7 -            val {T = xT, thy, ...} = Thm.rep_cterm cx;
    21.8 +            val xT = #T (Thm.rep_cterm cx);
    21.9              val ct = cert (tune t);
   21.10 +            val tT = Thm.ctyp_of_term ct;
   21.11            in
   21.12 -            if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
   21.13 +            if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct)
   21.14              else error (Pretty.string_of (Pretty.block
   21.15               [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
   21.16                Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
   21.17 @@ -432,7 +433,8 @@
   21.18  
   21.19  fun guess_instance rule i st =
   21.20    let
   21.21 -    val {thy, maxidx, ...} = Thm.rep_thm st;
   21.22 +    val thy = Thm.theory_of_thm st;
   21.23 +    val maxidx = Thm.maxidx_of st;
   21.24      val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
   21.25      val params = rev (rename_wrt_term goal (Logic.strip_params goal));
   21.26    in