src/HOL/Import/proof_kernel.ML
changeset 26626 c6231d64d264
parent 26343 0dd2eab7b296
child 26928 ca87aff1ad2d
     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