tuned;
authorwenzelm
Wed Jul 13 16:07:24 2005 +0200 (2005-07-13)
changeset 16803014090d1e64b
parent 16802 6eeee59dac4c
child 16804 3c339e1c069b
tuned;
src/HOL/Tools/ATP/recon_prelim.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/res_skolem_function.ML
src/HOL/Tools/res_types_sorts.ML
src/Pure/General/scan.ML
src/Pure/theory.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_prelim.ML	Wed Jul 13 16:07:23 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_prelim.ML	Wed Jul 13 16:07:24 2005 +0200
     1.3 @@ -3,29 +3,30 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 -val gcounter = ref 0; 
     1.8 -
     1.9 +structure ReconPrelim =
    1.10 +struct
    1.11  
    1.12  fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
    1.13  
    1.14  fun dest_neg(Const("Not",_) $ M) = M
    1.15    | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
    1.16  
    1.17 +fun iscomb a =
    1.18 +    if is_Free a then
    1.19 +      false
    1.20 +    else if is_Var a then
    1.21 +      false
    1.22 +    else if USyntax.is_conj a then
    1.23 +      false
    1.24 +    else if USyntax.is_disj a then
    1.25 +      false
    1.26 +    else if USyntax.is_forall a then
    1.27 +      false
    1.28 +    else if USyntax.is_exists a then
    1.29 +      false
    1.30 +    else
    1.31 +      true;
    1.32  
    1.33 -fun iscomb a = if is_Free a then
    1.34 -			false
    1.35 -	      else if is_Var a then
    1.36 -			false
    1.37 -		else if USyntax.is_conj a then
    1.38 -			false
    1.39 -		else if USyntax.is_disj a then
    1.40 -			false
    1.41 -		else if USyntax.is_forall a then
    1.42 -			false
    1.43 -		else if USyntax.is_exists a then
    1.44 -			false
    1.45 -		else
    1.46 -			true;
    1.47  fun getstring (Var (v,T)) = fst v
    1.48     |getstring (Free (v,T))= v;
    1.49  
    1.50 @@ -37,123 +38,95 @@
    1.51  
    1.52  fun fstequal a b = a = fst b;
    1.53  
    1.54 -fun takeout (i,[])  = []
    1.55 -   | takeout (i,(x::xs)) = if (i>0) then
    1.56 -                               (x::(takeout(i-1,xs)))
    1.57 -                           else
    1.58 -                               [];
    1.59 -		
    1.60 -
    1.61 -
    1.62  (* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
    1.63  fun is_Abs (Abs _) = true
    1.64    | is_Abs _ = false;
    1.65  fun is_Bound (Bound _) = true
    1.66    | is_Bound _ = false;
    1.67  
    1.68 -
    1.69 -
    1.70 -
    1.71  fun is_hol_tm t =
    1.72 -                if (is_Free t) then 
    1.73 -                        true 
    1.74 -                else if (is_Var t) then
    1.75 -                        true
    1.76 -                else if (is_Const t) then
    1.77 -                        true
    1.78 -                else if (is_Abs t) then
    1.79 -                        true
    1.80 -                else if (is_Bound t) then
    1.81 -                        true
    1.82 -                else 
    1.83 -                        let val (f, args) = strip_comb t in
    1.84 -                            if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then 
    1.85 -                                true            (* should be is_const *)
    1.86 -                            else 
    1.87 -                                false
    1.88 -                       end;
    1.89 +    if (is_Free t) then
    1.90 +      true
    1.91 +    else if (is_Var t) then
    1.92 +      true
    1.93 +    else if (is_Const t) then
    1.94 +      true
    1.95 +    else if (is_Abs t) then
    1.96 +      true
    1.97 +    else if (is_Bound t) then
    1.98 +      true
    1.99 +    else
   1.100 +      let val (f, args) = strip_comb t in
   1.101 +        if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
   1.102 +          true            (* should be is_const *)
   1.103 +        else
   1.104 +          false
   1.105 +      end;
   1.106  
   1.107 -fun is_hol_fm f =  if USyntax.is_neg f then
   1.108 -                        let val newf = USyntax.dest_neg f in
   1.109 -                            is_hol_fm newf
   1.110 -                        end
   1.111 -                    
   1.112 -               else if USyntax.is_disj f then
   1.113 -                        let val {disj1,disj2} = USyntax.dest_disj f in
   1.114 -                            (is_hol_fm disj1) andalso (is_hol_fm disj2)  (* shouldn't this be and ? *)
   1.115 -                        end 
   1.116 -               else if USyntax.is_conj f then
   1.117 -                        let val {conj1,conj2} = USyntax.dest_conj f in
   1.118 -                            (is_hol_fm conj1) andalso (is_hol_fm conj2)
   1.119 -                        end 
   1.120 -               else if (USyntax.is_forall f) then
   1.121 -                        let val {Body, Bvar} = USyntax.dest_forall f in
   1.122 -                            is_hol_fm Body
   1.123 -                        end
   1.124 -               else if (USyntax.is_exists f) then
   1.125 -                        let val {Body, Bvar} = USyntax.dest_exists f in
   1.126 -                            is_hol_fm Body
   1.127 -                        end
   1.128 -               else if (iscomb f) then
   1.129 -                        let val (P, args) = strip_comb f in
   1.130 -                            ((is_hol_tm P)) andalso (forall is_hol_fm args)
   1.131 -                        end
   1.132 -                else
   1.133 -                        is_hol_tm f;                              (* should be is_const, nee
   1.134 -d to check args *)
   1.135 -               
   1.136 +fun is_hol_fm f =
   1.137 +    if USyntax.is_neg f then
   1.138 +      let val newf = USyntax.dest_neg f in
   1.139 +        is_hol_fm newf
   1.140 +      end
   1.141 +    else if USyntax.is_disj f then
   1.142 +      let val {disj1,disj2} = USyntax.dest_disj f in
   1.143 +        (is_hol_fm disj1) andalso (is_hol_fm disj2)  (* shouldn't this be and ? *)
   1.144 +      end
   1.145 +    else if USyntax.is_conj f then
   1.146 +      let val {conj1,conj2} = USyntax.dest_conj f in
   1.147 +        (is_hol_fm conj1) andalso (is_hol_fm conj2)
   1.148 +      end
   1.149 +    else if (USyntax.is_forall f) then
   1.150 +      let val {Body, Bvar} = USyntax.dest_forall f in
   1.151 +        is_hol_fm Body
   1.152 +      end
   1.153 +    else if (USyntax.is_exists f) then
   1.154 +      let val {Body, Bvar} = USyntax.dest_exists f in
   1.155 +        is_hol_fm Body
   1.156 +      end
   1.157 +    else if (iscomb f) then
   1.158 +      let val (P, args) = strip_comb f in
   1.159 +        ((is_hol_tm P)) andalso (forall is_hol_fm args)
   1.160 +      end
   1.161 +    else
   1.162 +      is_hol_tm f;           (* should be is_const, need to check args *)
   1.163  
   1.164 -fun hol_literal t = 
   1.165 -   (is_hol_fm t) andalso 
   1.166 -   ( not ((USyntax.is_conj t) orelse (USyntax.is_disj t) orelse (USyntax.is_forall t) orelse (USyntax.is_exists t)));
   1.167 -
   1.168 -
   1.169 +fun hol_literal t =
   1.170 +  is_hol_fm t andalso
   1.171 +    (not (USyntax.is_conj t orelse USyntax.is_disj t orelse USyntax.is_forall t
   1.172 +      orelse USyntax.is_exists t));
   1.173  
   1.174  
   1.175  (*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
   1.176 -fun getcombvar a = let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
   1.177 -			if (iscomb rand) then
   1.178 -				getcombvar rand
   1.179 -			else
   1.180 -				rand
   1.181 -		   end;
   1.182 -
   1.183 -
   1.184 -
   1.185 -fun free2var v = let val thing = dest_Free v 
   1.186 -                     val (name,vtype) = thing
   1.187 -                     val index = (name,0) in
   1.188 -                     Var (index,vtype)
   1.189 -                 end;
   1.190 +fun getcombvar a =
   1.191 +    let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
   1.192 +      if (iscomb rand) then
   1.193 +        getcombvar rand
   1.194 +      else
   1.195 +        rand
   1.196 +    end;
   1.197  
   1.198 -fun var2free v = let val (index, tv) = dest_Var v 
   1.199 -                     val istr = fst index in
   1.200 -                     Free (istr,tv)
   1.201 -                 end;
   1.202 -
   1.203 -fun is_empty_seq thisseq =  case Seq.chop (1, thisseq) of
   1.204 -                             ([],_)   => true
   1.205 -                           |      _   => false
   1.206 +fun free2var v =
   1.207 +  let val (name, vtype) = dest_Free v
   1.208 +  in Var ((name, 0), vtype) end;
   1.209  
   1.210 -fun getnewenv thisseq = 
   1.211 -			   let val seqlist = Seq.list_of thisseq
   1.212 -			   val envpair =hd seqlist in
   1.213 -			   fst envpair 
   1.214 -			end;
   1.215 +fun var2free v =
   1.216 +  let val ((x, _), tv) = dest_Var v
   1.217 +  in Free (x, tv) end;
   1.218  
   1.219 -fun getnewsubsts thisseq =  let val seqlist = Seq.list_of thisseq
   1.220 -			   val envpair =hd seqlist in
   1.221 -			   snd envpair 
   1.222 -			end;
   1.223 +val is_empty_seq = is_none o Seq.pull;
   1.224  
   1.225 -
   1.226 +fun getnewenv seq = fst (fst (the (Seq.pull seq)));
   1.227 +fun getnewsubsts seq = snd (fst (the (Seq.pull seq)));
   1.228  
   1.229  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
   1.230  
   1.231 -
   1.232 +fun int_of_string str =
   1.233 +  (case Int.fromString str of SOME n => n
   1.234 +  | NONE => error ("int_of_string: " ^ str));
   1.235  
   1.236 -fun int_of_string str = valOf (Int.fromString str)
   1.237 -                        handle Option => error ("int_of_string: " ^ str);
   1.238 -    
   1.239 -                	 
   1.240 +val no_lines = filter_out (equal "\n");
   1.241 +
   1.242  exception ASSERTION of string;
   1.243 +
   1.244 +end;
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jul 13 16:07:23 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jul 13 16:07:24 2005 +0200
     2.3 @@ -9,11 +9,11 @@
     2.4  
     2.5  structure Recon_Transfer =
     2.6  struct
     2.7 +
     2.8  open Recon_Parse
     2.9 +
    2.10  infixr 8 ++; infixr 7 >>; infixr 6 ||;
    2.11  
    2.12 -fun not_newline ch = not (ch = "\n");
    2.13 -
    2.14  
    2.15  
    2.16  (*
    2.17 @@ -51,14 +51,9 @@
    2.18  
    2.19  (* Versions that include type information *)
    2.20   
    2.21 +(* FIXME rename to str_of_thm *)
    2.22  fun string_of_thm thm =
    2.23 -  let val _ = set show_sorts
    2.24 -      val str = Display.string_of_thm thm
    2.25 -      val no_returns =List.filter not_newline (explode str)
    2.26 -      val _ = reset show_sorts
    2.27 -  in 
    2.28 -      implode no_returns
    2.29 -  end
    2.30 +  setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm;
    2.31  
    2.32  
    2.33  (* check separate args in the watcher program for separating strings with a * or ; or something *)
    2.34 @@ -377,31 +372,16 @@
    2.35  \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
    2.36  \1454[0:Obv:1453.0] ||  -> .";*)
    2.37  
    2.38 -fun remove_linebreaks str = let val strlist = explode str
    2.39 -	                        val nonewlines = filter (not_equal "\n") strlist
    2.40 -	                    in
    2.41 -				implode nonewlines
    2.42 -			    end
    2.43 -
    2.44 +fun subst_for a b [] = ""
    2.45 +  | subst_for a b (x :: xs) =
    2.46 +      if x = a
    2.47 +      then 
    2.48 +	b ^ subst_for a b xs
    2.49 +      else
    2.50 +	x ^ subst_for a b xs;
    2.51  
    2.52 -fun subst_for a b [] = ""
    2.53 -|   subst_for a b (x::xs) = if (x = a)
    2.54 -				   then 
    2.55 -					(b^(subst_for a b  xs))
    2.56 -				   else
    2.57 -					x^(subst_for a b xs)
    2.58 -
    2.59 -
    2.60 -fun remove_linebreaks str = let val strlist = explode str
    2.61 -			    in
    2.62 -				subst_for "\n" "\t" strlist
    2.63 -			    end
    2.64 -
    2.65 -fun restore_linebreaks str = let val strlist = explode str
    2.66 -			     in
    2.67 -				subst_for "\t" "\n" strlist
    2.68 -			     end
    2.69 -
    2.70 +val remove_linebreaks = subst_for "\n" "\t" o explode;
    2.71 +val restore_linebreaks = subst_for "\t" "\n" o explode;
    2.72  
    2.73  
    2.74  fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
     3.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Jul 13 16:07:23 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Jul 13 16:07:24 2005 +0200
     3.3 @@ -3,6 +3,11 @@
     3.4      Copyright   2004  University of Cambridge
     3.5  *)
     3.6  
     3.7 +structure ReconTranslateProof =
     3.8 +struct
     3.9 +
    3.10 +open ReconPrelim;
    3.11 +
    3.12  fun add_in_order (x:string) [] = [x]
    3.13  |   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
    3.14                               then 
    3.15 @@ -15,10 +20,6 @@
    3.16       
    3.17  fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
    3.18  
    3.19 -Goal "False ==> False";
    3.20 -by Auto_tac;
    3.21 -qed "False_imp";
    3.22 -
    3.23  exception Reflex_equal;
    3.24  
    3.25  (********************************)
    3.26 @@ -28,7 +29,7 @@
    3.27  
    3.28  datatype Side = Left |Right
    3.29  
    3.30 - datatype Proofstep =  ExtraAxiom
    3.31 +datatype Proofstep =  ExtraAxiom
    3.32                       | OrigAxiom
    3.33    		     | VampInput 
    3.34                       | Axiom
    3.35 @@ -424,15 +425,13 @@
    3.36                      end
    3.37  
    3.38  
    3.39 -fun not_newline ch = not (ch = "\n");
    3.40 -
    3.41  (*
    3.42  
    3.43  fun follow clauses [] allvars thml recons = 
    3.44                               let (* val _ = reset show_sorts*)
    3.45                                val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
    3.46                                val thmproofstring = proofstring ( thmstring)
    3.47 -                            val no_returns =List.filter  not_newline ( thmproofstring)
    3.48 +                            val no_returns = no_lines thmproofstring
    3.49                              val thmstr = implode no_returns
    3.50                                 val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file")))
    3.51                                 val _ = TextIO.output(outfile, "thmstr is "^thmstr)
    3.52 @@ -502,3 +501,5 @@
    3.53  fun remove_tinfo [] = []
    3.54    | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
    3.55        (clausenum, step , newstrs)::(remove_tinfo xs)
    3.56 +
    3.57 +end;
     4.1 --- a/src/HOL/Tools/res_skolem_function.ML	Wed Jul 13 16:07:23 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_skolem_function.ML	Wed Jul 13 16:07:24 2005 +0200
     4.3 @@ -2,55 +2,28 @@
     4.4      ID: $Id$
     4.5      Copyright 2004 University of Cambridge
     4.6  
     4.7 -Generation of unique Skolem functions (with types) as Term.term.
     4.8 +Generation of unique Skolem functions (with types) as term.
     4.9  *)
    4.10  
    4.11  signature RES_SKOLEM_FUNCTION =
    4.12  sig
    4.13 -
    4.14 -val gen_skolem: Term.term list -> Term.typ  -> Term.term
    4.15 -
    4.16 +  val gen_skolem: term list -> typ -> term
    4.17  end;
    4.18  
    4.19  structure ResSkolemFunction: RES_SKOLEM_FUNCTION  =
    4.20 -
    4.21  struct
    4.22  
    4.23  val skolem_prefix = "sk_";
    4.24 -
    4.25 -(* internal reference starting from 0. *)
    4.26  val skolem_id = ref 0;
    4.27  
    4.28 -
    4.29 -fun gen_skolem_name () = 
    4.30 -    let val new_id = !skolem_id
    4.31 -	val sk_fun = skolem_prefix ^ (string_of_int new_id)
    4.32 -    in
    4.33 -	(skolem_id := new_id + 1; sk_fun) (* increment id by 1. *)
    4.34 -    end;
    4.35 -
    4.36 -fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp])
    4.37 -  | sk_type_of_aux (Var(_,tp1)::vars) tp = 
    4.38 -    let val tp' = sk_type_of_aux vars tp
    4.39 -    in
    4.40 -	Type("fun",[tp1,tp'])
    4.41 -    end;
    4.42 -
    4.43 +fun gen_skolem_name () =
    4.44 +  let val sk_fun = skolem_prefix ^ string_of_int (! skolem_id);
    4.45 +  in inc skolem_id; sk_fun end;
    4.46  
    4.47 -fun sk_type_of [] tp = tp
    4.48 -  | sk_type_of vars tp = sk_type_of_aux vars tp; 
    4.49 -
    4.50 -
    4.51 +fun gen_skolem univ_vars tp =
    4.52 +  let
    4.53 +    val skolem_type = map Term.fastype_of univ_vars ---> tp
    4.54 +    val skolem_term = Const (gen_skolem_name (), skolem_type)
    4.55 +  in Term.list_comb (skolem_term, univ_vars) end;
    4.56  
    4.57 -fun gen_skolem univ_vars tp = 
    4.58 -    let val new_sk_name = gen_skolem_name ()
    4.59 -	val new_sk_type = sk_type_of univ_vars tp
    4.60 -	val skolem_term = Const(new_sk_name,new_sk_type)
    4.61 -	fun app [] sf = sf
    4.62 -	  | app (var::vars) sf= app vars (sf $ var)
    4.63 -    in
    4.64 -	app univ_vars skolem_term
    4.65 -    end;
    4.66 -
    4.67 -
    4.68 -end;
    4.69 \ No newline at end of file
    4.70 +end;
     5.1 --- a/src/HOL/Tools/res_types_sorts.ML	Wed Jul 13 16:07:23 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_types_sorts.ML	Wed Jul 13 16:07:24 2005 +0200
     5.3 @@ -10,20 +10,16 @@
     5.4  sig
     5.5    exception ARITIES of string
     5.6    val arity_clause: string * (string * string list list) list -> ResClause.arityClause list
     5.7 -  val arity_clause_sg: Sign.sg -> ResClause.arityClause list list * (string * 'a list) list
     5.8    val arity_clause_thy: theory -> ResClause.arityClause list list * (string * 'a list) list
     5.9    type classrelClauses
    5.10    val classrel_clause: string * string list -> ResClause.classrelClause list
    5.11    val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list
    5.12 -  val classrel_clauses_sg: Sign.sg -> ResClause.classrelClause list list
    5.13    val classrel_clauses_thy: theory -> ResClause.classrelClause list list
    5.14 -  val classrel_of_sg: Sign.sg -> Sorts.classes
    5.15    val multi_arity_clause:
    5.16      (string * (string * string list list) list) list ->
    5.17      (string * 'a list) list ->
    5.18      ResClause.arityClause list list * (string * 'a list) list
    5.19    val tptp_arity_clause_thy: theory -> string list list
    5.20 -  val tptp_classrel_clauses_sg : Sign.sg -> string list list
    5.21  end;
    5.22  
    5.23  structure ResTypesSorts: RES_TYPES_SORTS =
    5.24 @@ -45,12 +41,10 @@
    5.25        let val result = multi_arity_clause tcons_ars expts
    5.26        in ((arity_clause tcon_ar :: fst result), snd result) end;
    5.27  
    5.28 -fun arity_clause_sg sg =
    5.29 -  let val arities = #arities (Type.rep_tsig (Sign.tsig_of sg))
    5.30 +fun arity_clause_thy thy =
    5.31 +  let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
    5.32    in multi_arity_clause (Symtab.dest arities) [] end;
    5.33  
    5.34 -fun arity_clause_thy thy = arity_clause_sg (Theory.sign_of thy);
    5.35 -
    5.36  fun tptp_arity_clause_thy thy =
    5.37    map (map ResClause.tptp_arity_clause) (#1 (arity_clause_thy thy));
    5.38  
    5.39 @@ -59,13 +53,12 @@
    5.40  
    5.41  type classrelClauses = ResClause.classrelClause list Symtab.table;
    5.42  
    5.43 -val classrel_of_sg = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
    5.44 +val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
    5.45  val classrel_clause = ResClause.classrelClauses_of;
    5.46  fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C);
    5.47 -val classrel_clauses_sg = classrel_clauses_classrel o classrel_of_sg;
    5.48 -val classrel_clauses_thy = classrel_clauses_sg o Theory.sign_of;
    5.49 +val classrel_clauses_thy = classrel_clauses_classrel o classrel_of;
    5.50  
    5.51 -val tptp_classrel_clauses_sg =
    5.52 -  map (map ResClause.tptp_classrelClause) o classrel_clauses_sg;
    5.53 +val tptp_classrel_clauses_thy =
    5.54 +  map (map ResClause.tptp_classrelClause) o classrel_clauses_thy;
    5.55  
    5.56  end;
     6.1 --- a/src/Pure/General/scan.ML	Wed Jul 13 16:07:23 2005 +0200
     6.2 +++ b/src/Pure/General/scan.ML	Wed Jul 13 16:07:24 2005 +0200
     6.3 @@ -259,7 +259,7 @@
     6.4    in
     6.5      if exists is_stopper input then
     6.6        raise ABORT "Stopper may not occur in input of finite scan!"
     6.7 -    else (force scan --| lift stop) (state, List.revAppend (rev input, [stopper]))
     6.8 +    else (force scan --| lift stop) (state, input @ [stopper])
     6.9    end;
    6.10  
    6.11  fun finite stopper scan = unlift (finite' stopper (lift scan));
     7.1 --- a/src/Pure/theory.ML	Wed Jul 13 16:07:23 2005 +0200
     7.2 +++ b/src/Pure/theory.ML	Wed Jul 13 16:07:24 2005 +0200
     7.3 @@ -179,7 +179,7 @@
     7.4  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
     7.5  fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
     7.6  
     7.7 -fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D)
     7.8 +val defs_of = #defs o rep_theory;
     7.9  
    7.10  fun requires thy name what =
    7.11    if Context.exists_name name thy then ()