avoid low-level tsig;
authorwenzelm
Tue Aug 14 23:22:51 2007 +0200 (2007-08-14)
changeset 24271499608101177
parent 24270 f53b7dab4426
child 24272 2f85bae2e2c2
avoid low-level tsig;
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Tools/lin_arith.ML
src/Pure/axclass.ML
src/Tools/Compute_Oracle/linker.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Aug 14 23:22:49 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Aug 14 23:22:51 2007 +0200
     1.3 @@ -78,8 +78,7 @@
     1.4     val goal = List.nth(prems_of thm, i-1);
     1.5     val ps = Logic.strip_params goal;
     1.6     val Ts = rev (map snd ps);
     1.7 -   fun is_of_fs_name T = Type.of_sort (Sign.tsig_of thy)
     1.8 -     (T, Sign.intern_sort thy ["fs_"^atom_basename]); 
     1.9 +   fun is_of_fs_name T = Sign.of_sort thy (T, Sign.intern_sort thy ["fs_"^atom_basename]); 
    1.10  (* rebuild de bruijn indices *)
    1.11     val bvs = map_index (Bound o fst) ps;
    1.12  (* select variables of the right class *)
     2.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Tue Aug 14 23:22:49 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Tue Aug 14 23:22:51 2007 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4                  (* FIXME: this should be an operation the library *)
     2.5                  val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
     2.6               in
     2.7 -                if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
     2.8 +                if (Sign.of_sort thy (ty,[class_name]))
     2.9                  then [(pi,typi)]
    2.10                  else raise
    2.11                  EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Tue Aug 14 23:22:49 2007 +0200
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Tue Aug 14 23:22:51 2007 +0200
     3.3 @@ -266,8 +266,8 @@
     3.4    | _                   => NONE
     3.5  end handle Zero => NONE;
     3.6  
     3.7 -fun of_lin_arith_sort sg (U : typ) : bool =
     3.8 -  Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"])
     3.9 +fun of_lin_arith_sort thy U =
    3.10 +  Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]);
    3.11  
    3.12  fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
    3.13    if of_lin_arith_sort sg U then
     4.1 --- a/src/Pure/axclass.ML	Tue Aug 14 23:22:49 2007 +0200
     4.2 +++ b/src/Pure/axclass.ML	Tue Aug 14 23:22:51 2007 +0200
     4.3 @@ -189,7 +189,7 @@
     4.4  fun cert_classrel thy raw_rel =
     4.5    let
     4.6      val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
     4.7 -    val _ = Type.add_classrel (Sign.pp thy) (c1, c2) (Sign.tsig_of thy);
     4.8 +    val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy);
     4.9      val _ =
    4.10        (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
    4.11          [] => ()
     5.1 --- a/src/Tools/Compute_Oracle/linker.ML	Tue Aug 14 23:22:49 2007 +0200
     5.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Tue Aug 14 23:22:51 2007 +0200
     5.3 @@ -1,35 +1,38 @@
     5.4  (*  Title:      Tools/Compute_Oracle/Linker.ML
     5.5 -    ID:         $$
     5.6 +    ID:         $Id$
     5.7      Author:     Steven Obua
     5.8  
     5.9 -    Linker.ML solves the problem that the computing oracle does not instantiate polymorphic rules.
    5.10 -    By going through the PCompute interface, all possible instantiations are resolved by compiling new programs, if necessary.
    5.11 -    The obvious disadvantage of this approach is that in the worst case for each new term to be rewritten, a new program may be compiled.
    5.12 +Linker.ML solves the problem that the computing oracle does not
    5.13 +instantiate polymorphic rules. By going through the PCompute interface,
    5.14 +all possible instantiations are resolved by compiling new programs, if
    5.15 +necessary. The obvious disadvantage of this approach is that in the
    5.16 +worst case for each new term to be rewritten, a new program may be
    5.17 +compiled.
    5.18  *)
    5.19  
    5.20 -(*    
    5.21 +(*
    5.22     Given constants/frees c_1::t_1, c_2::t_2, ...., c_n::t_n,
    5.23     and constants/frees d_1::d_1, d_2::s_2, ..., d_m::s_m
    5.24  
    5.25     Find all substitutions S such that
    5.26 -   a) the domain of S is tvars (t_1, ..., t_n)   
    5.27 +   a) the domain of S is tvars (t_1, ..., t_n)
    5.28     b) there are indices i_1, ..., i_k, and j_1, ..., j_k with
    5.29        1. S (c_i_1::t_i_1) = d_j_1::s_j_1, ..., S (c_i_k::t_i_k) = d_j_k::s_j_k
    5.30        2. tvars (t_i_1, ..., t_i_k) = tvars (t_1, ..., t_n)
    5.31  *)
    5.32 -signature LINKER = 
    5.33 +signature LINKER =
    5.34  sig
    5.35      exception Link of string
    5.36 -    
    5.37 +
    5.38      datatype constant = Constant of bool * string * typ
    5.39      val constant_of : term -> constant
    5.40  
    5.41      type instances
    5.42      type subst = Type.tyenv
    5.43 -    
    5.44 +
    5.45      val empty : constant list -> instances
    5.46      val typ_of_constant : constant -> typ
    5.47 -    val add_instances : Type.tsig -> instances -> constant list -> subst list * instances
    5.48 +    val add_instances : theory -> instances -> constant list -> subst list * instances
    5.49      val substs_of : instances -> subst list
    5.50      val is_polymorphic : constant -> bool
    5.51      val distinct_constants : constant list -> constant list
    5.52 @@ -59,15 +62,15 @@
    5.53  
    5.54  val empty_subst = (Vartab.empty : Type.tyenv)
    5.55  
    5.56 -fun merge_subst (A:Type.tyenv) (B:Type.tyenv) = 
    5.57 -    SOME (Vartab.fold (fn (v, t) => 
    5.58 -		       fn tab => 
    5.59 -			  (case Vartab.lookup tab v of 
    5.60 -			       NONE => Vartab.update (v, t) tab 
    5.61 -			     | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
    5.62 +fun merge_subst (A:Type.tyenv) (B:Type.tyenv) =
    5.63 +    SOME (Vartab.fold (fn (v, t) =>
    5.64 +                       fn tab =>
    5.65 +                          (case Vartab.lookup tab v of
    5.66 +                               NONE => Vartab.update (v, t) tab
    5.67 +                             | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
    5.68      handle Type.TYPE_MATCH => NONE
    5.69  
    5.70 -fun subst_ord (A:Type.tyenv, B:Type.tyenv) = 
    5.71 +fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
    5.72      (list_ord (prod_ord Term.fast_indexname_ord (prod_ord Term.sort_ord Term.typ_ord))) (Vartab.dest A, Vartab.dest B)
    5.73  
    5.74  structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
    5.75 @@ -79,113 +82,113 @@
    5.76  
    5.77  datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
    5.78  
    5.79 -fun is_polymorphic (Constant (_, _, ty)) = not (null (typ_tvars ty))		
    5.80 +fun is_polymorphic (Constant (_, _, ty)) = not (null (typ_tvars ty))
    5.81  
    5.82  fun distinct_constants cs =
    5.83      Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
    5.84  
    5.85 -fun empty cs = 
    5.86 -    let				   
    5.87 -	val cs = distinct_constants (filter is_polymorphic cs)
    5.88 -	val old_cs = cs
    5.89 -(*	fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (typ_tvars ty) tab
    5.90 -	val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
    5.91 -	fun tvars_of ty = collect_tvars ty Typtab.empty
    5.92 -	val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
    5.93 +fun empty cs =
    5.94 +    let
    5.95 +        val cs = distinct_constants (filter is_polymorphic cs)
    5.96 +        val old_cs = cs
    5.97 +(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (typ_tvars ty) tab
    5.98 +        val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
    5.99 +        fun tvars_of ty = collect_tvars ty Typtab.empty
   5.100 +        val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
   5.101  
   5.102 -	fun tyunion A B = 
   5.103 -	    Typtab.fold 
   5.104 -		(fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
   5.105 -		A B
   5.106 +        fun tyunion A B =
   5.107 +            Typtab.fold
   5.108 +                (fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
   5.109 +                A B
   5.110  
   5.111          fun is_essential A B =
   5.112 -	    Typtab.fold
   5.113 -	    (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
   5.114 -	    A false
   5.115 +            Typtab.fold
   5.116 +            (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
   5.117 +            A false
   5.118  
   5.119 -	fun add_minimal (c', tvs') (tvs, cs) =
   5.120 -	    let
   5.121 -		val tvs = tyunion tvs' tvs
   5.122 -		val cs = (c', tvs')::cs
   5.123 -	    in
   5.124 -		if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
   5.125 -		    SOME (tvs, cs)
   5.126 -		else 
   5.127 -		    NONE
   5.128 -	    end
   5.129 +        fun add_minimal (c', tvs') (tvs, cs) =
   5.130 +            let
   5.131 +                val tvs = tyunion tvs' tvs
   5.132 +                val cs = (c', tvs')::cs
   5.133 +            in
   5.134 +                if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
   5.135 +                    SOME (tvs, cs)
   5.136 +                else
   5.137 +                    NONE
   5.138 +            end
   5.139  
   5.140 -	fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)
   5.141 +        fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)
   5.142  
   5.143 -	fun generate_minimal_subsets subsets [] = subsets
   5.144 -	  | generate_minimal_subsets subsets (c::cs) = 
   5.145 -	    let
   5.146 -		val subsets' = map_filter (add_minimal c) subsets
   5.147 -	    in
   5.148 -		generate_minimal_subsets (subsets@subsets') cs
   5.149 -	    end*)
   5.150 +        fun generate_minimal_subsets subsets [] = subsets
   5.151 +          | generate_minimal_subsets subsets (c::cs) =
   5.152 +            let
   5.153 +                val subsets' = map_filter (add_minimal c) subsets
   5.154 +            in
   5.155 +                generate_minimal_subsets (subsets@subsets') cs
   5.156 +            end*)
   5.157  
   5.158 -	val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)
   5.159 +        val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)
   5.160  
   5.161 -	val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)
   5.162 +        val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)
   5.163  
   5.164      in
   5.165 -	Instances (
   5.166 -	fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
   5.167 -	Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants), 
   5.168 -	minimal_subsets, Substtab.empty)
   5.169 +        Instances (
   5.170 +        fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
   5.171 +        Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants),
   5.172 +        minimal_subsets, Substtab.empty)
   5.173      end
   5.174  
   5.175  local
   5.176  fun calc ctab substtab [] = substtab
   5.177 -  | calc ctab substtab (c::cs) = 
   5.178 +  | calc ctab substtab (c::cs) =
   5.179      let
   5.180 -	val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
   5.181 -	fun merge_substs substtab subst = 
   5.182 -	    Substtab.fold (fn (s,_) => 
   5.183 -			   fn tab => 
   5.184 -			      (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
   5.185 -			  substtab Substtab.empty
   5.186 -	val substtab = substtab_unions (map (merge_substs substtab) csubsts)
   5.187 +        val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
   5.188 +        fun merge_substs substtab subst =
   5.189 +            Substtab.fold (fn (s,_) =>
   5.190 +                           fn tab =>
   5.191 +                              (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
   5.192 +                          substtab Substtab.empty
   5.193 +        val substtab = substtab_unions (map (merge_substs substtab) csubsts)
   5.194      in
   5.195 -	calc ctab substtab cs
   5.196 +        calc ctab substtab cs
   5.197      end
   5.198  in
   5.199  fun calc_substs ctab (cs:constant list) = calc ctab (Substtab.update (empty_subst, ()) Substtab.empty) cs
   5.200  end
   5.201 -	      			    
   5.202 -fun add_instances tsig (Instances (cfilter, ctab,minsets,substs)) cs = 
   5.203 -    let	
   5.204 -(*	val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
   5.205 -	fun calc_instantiations (constant as Constant (free, name, ty)) instantiations = 
   5.206 -	    Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>  
   5.207 -			   fn instantiations =>
   5.208 -			      if free <> free' orelse name <> name' then
   5.209 -				  instantiations
   5.210 -			      else case Consttab.lookup insttab constant of
   5.211 -				       SOME _ => instantiations
   5.212 -				     | NONE => ((constant', (constant, Type.typ_match tsig (ty', ty) empty_subst))::instantiations
   5.213 -						handle TYPE_MATCH => instantiations))
   5.214 -			  ctab instantiations
   5.215 -	val instantiations = fold calc_instantiations cs []
   5.216 -	(*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
   5.217 -	fun update_ctab (constant', entry) ctab = 
   5.218 -	    (case Consttab.lookup ctab constant' of
   5.219 -		 NONE => raise Link "internal error: update_ctab"
   5.220 -	       | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
   5.221 -	val ctab = fold update_ctab instantiations ctab	
   5.222 -	val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs) 
   5.223 -			      minsets Substtab.empty
   5.224 -	val (added_substs, substs) = 
   5.225 -	    Substtab.fold (fn (ns, _) => 
   5.226 -			   fn (added, substtab) => 
   5.227 -			      (case Substtab.lookup substs ns of
   5.228 -				   NONE => (ns::added, Substtab.update (ns, ()) substtab)
   5.229 -				 | SOME () => (added, substtab)))
   5.230 -			  new_substs ([], substs)
   5.231 +
   5.232 +fun add_instances thy (Instances (cfilter, ctab,minsets,substs)) cs =
   5.233 +    let
   5.234 +(*      val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
   5.235 +        fun calc_instantiations (constant as Constant (free, name, ty)) instantiations =
   5.236 +            Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>
   5.237 +                           fn instantiations =>
   5.238 +                              if free <> free' orelse name <> name' then
   5.239 +                                  instantiations
   5.240 +                              else case Consttab.lookup insttab constant of
   5.241 +                                       SOME _ => instantiations
   5.242 +                                     | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
   5.243 +                                                handle TYPE_MATCH => instantiations))
   5.244 +                          ctab instantiations
   5.245 +        val instantiations = fold calc_instantiations cs []
   5.246 +        (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
   5.247 +        fun update_ctab (constant', entry) ctab =
   5.248 +            (case Consttab.lookup ctab constant' of
   5.249 +                 NONE => raise Link "internal error: update_ctab"
   5.250 +               | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
   5.251 +        val ctab = fold update_ctab instantiations ctab
   5.252 +        val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs)
   5.253 +                              minsets Substtab.empty
   5.254 +        val (added_substs, substs) =
   5.255 +            Substtab.fold (fn (ns, _) =>
   5.256 +                           fn (added, substtab) =>
   5.257 +                              (case Substtab.lookup substs ns of
   5.258 +                                   NONE => (ns::added, Substtab.update (ns, ()) substtab)
   5.259 +                                 | SOME () => (added, substtab)))
   5.260 +                          new_substs ([], substs)
   5.261      in
   5.262 -	(added_substs, Instances (cfilter, ctab, minsets, substs))
   5.263 +        (added_substs, Instances (cfilter, ctab, minsets, substs))
   5.264      end
   5.265 -	    	
   5.266 +
   5.267  
   5.268  fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
   5.269  
   5.270 @@ -196,7 +199,7 @@
   5.271    fun eq_to_meta th = (eq_th OF [th] handle _ => th)
   5.272  end
   5.273  
   5.274 -				     
   5.275 +
   5.276  local
   5.277  
   5.278  fun collect (Var x) tab = tab
   5.279 @@ -215,12 +218,12 @@
   5.280  sig
   5.281  
   5.282      type pcomputer
   5.283 -	 
   5.284 +
   5.285      val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer
   5.286  
   5.287  (*    val add_thms : pcomputer -> thm list -> bool*)
   5.288  
   5.289 -    val add_instances : pcomputer -> Linker.constant list -> bool 
   5.290 +    val add_instances : pcomputer -> Linker.constant list -> bool
   5.291  
   5.292      val rewrite : pcomputer -> cterm list -> thm list
   5.293  
   5.294 @@ -240,94 +243,93 @@
   5.295    | collect_consts (Abs (_, _, body)) = collect_consts body
   5.296    | collect_consts t = [Linker.constant_of t]*)
   5.297  
   5.298 -fun collect_consts_of_thm th = 
   5.299 +fun collect_consts_of_thm th =
   5.300      let
   5.301 -	val th = prop_of th
   5.302 -	val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th)
   5.303 -	val (left, right) = Logic.dest_equals th
   5.304 +        val th = prop_of th
   5.305 +        val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th)
   5.306 +        val (left, right) = Logic.dest_equals th
   5.307      in
   5.308 -	(Linker.collect_consts [left], Linker.collect_consts (right::prems))
   5.309 -    end 
   5.310 +        (Linker.collect_consts [left], Linker.collect_consts (right::prems))
   5.311 +    end
   5.312  
   5.313  fun create_theorem th =
   5.314 -let    
   5.315 +let
   5.316      val (left, right) = collect_consts_of_thm th
   5.317      val polycs = filter Linker.is_polymorphic left
   5.318      val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
   5.319 -    fun check_const (c::cs) cs' = 
   5.320 -	let
   5.321 -	    val tvars = typ_tvars (Linker.typ_of_constant c)
   5.322 -	    val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
   5.323 -	in
   5.324 -	    if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
   5.325 -	    else 
   5.326 -		if null (tvars) then
   5.327 -		    check_const cs (c::cs')
   5.328 -		else
   5.329 -		    check_const cs cs'
   5.330 -	end
   5.331 +    fun check_const (c::cs) cs' =
   5.332 +        let
   5.333 +            val tvars = typ_tvars (Linker.typ_of_constant c)
   5.334 +            val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
   5.335 +        in
   5.336 +            if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
   5.337 +            else
   5.338 +                if null (tvars) then
   5.339 +                    check_const cs (c::cs')
   5.340 +                else
   5.341 +                    check_const cs cs'
   5.342 +        end
   5.343        | check_const [] cs' = cs'
   5.344 -    val monocs = check_const right [] 
   5.345 +    val monocs = check_const right []
   5.346  in
   5.347 -    if null (polycs) then 
   5.348 -	(monocs, MonoThm th)
   5.349 +    if null (polycs) then
   5.350 +        (monocs, MonoThm th)
   5.351      else
   5.352 -	(monocs, PolyThm (th, Linker.empty polycs, []))
   5.353 +        (monocs, PolyThm (th, Linker.empty polycs, []))
   5.354  end
   5.355  
   5.356 -fun create_computer machine thy ths = 
   5.357 +fun create_computer machine thy ths =
   5.358      let
   5.359 -	fun add (MonoThm th) ths = th::ths
   5.360 -	  | add (PolyThm (_, _, ths')) ths = ths'@ths
   5.361 -	val ths = fold_rev add ths []
   5.362 +        fun add (MonoThm th) ths = th::ths
   5.363 +          | add (PolyThm (_, _, ths')) ths = ths'@ths
   5.364 +        val ths = fold_rev add ths []
   5.365      in
   5.366 -	Compute.make machine thy ths
   5.367 +        Compute.make machine thy ths
   5.368      end
   5.369  
   5.370  fun conv_subst thy (subst : Type.tyenv) =
   5.371      map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst)
   5.372  
   5.373 -fun add_monos thy monocs ths = 
   5.374 +fun add_monos thy monocs ths =
   5.375      let
   5.376 -	val tsig = Sign.tsig_of thy
   5.377 -	val changed = ref false
   5.378 -	fun add monocs (th as (MonoThm _)) = ([], th)
   5.379 -	  | add monocs (PolyThm (th, instances, instanceths)) = 
   5.380 -	    let
   5.381 -		val (newsubsts, instances) = Linker.add_instances tsig instances monocs
   5.382 -		val _ = if not (null newsubsts) then changed := true else ()
   5.383 -		val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
   5.384 -(*		val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
   5.385 -		val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
   5.386 -	    in
   5.387 -		(newmonos, PolyThm (th, instances, instanceths@newths))
   5.388 -	    end
   5.389 -	fun step monocs ths = 
   5.390 -	    fold_rev (fn th => 
   5.391 -		      fn (newmonos, ths) => 
   5.392 -			 let val (newmonos', th') = add monocs th in
   5.393 -			     (newmonos'@newmonos, th'::ths)
   5.394 -			 end)
   5.395 -		     ths ([], [])
   5.396 -	fun loop monocs ths = 
   5.397 -	    let val (monocs', ths') = step monocs ths in
   5.398 -		if null (monocs') then 
   5.399 -		    ths' 
   5.400 -		else 
   5.401 -		    loop monocs' ths'
   5.402 -	    end
   5.403 -	val result = loop monocs ths
   5.404 +        val changed = ref false
   5.405 +        fun add monocs (th as (MonoThm _)) = ([], th)
   5.406 +          | add monocs (PolyThm (th, instances, instanceths)) =
   5.407 +            let
   5.408 +                val (newsubsts, instances) = Linker.add_instances thy instances monocs
   5.409 +                val _ = if not (null newsubsts) then changed := true else ()
   5.410 +                val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
   5.411 +(*              val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
   5.412 +                val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
   5.413 +            in
   5.414 +                (newmonos, PolyThm (th, instances, instanceths@newths))
   5.415 +            end
   5.416 +        fun step monocs ths =
   5.417 +            fold_rev (fn th =>
   5.418 +                      fn (newmonos, ths) =>
   5.419 +                         let val (newmonos', th') = add monocs th in
   5.420 +                             (newmonos'@newmonos, th'::ths)
   5.421 +                         end)
   5.422 +                     ths ([], [])
   5.423 +        fun loop monocs ths =
   5.424 +            let val (monocs', ths') = step monocs ths in
   5.425 +                if null (monocs') then
   5.426 +                    ths'
   5.427 +                else
   5.428 +                    loop monocs' ths'
   5.429 +            end
   5.430 +        val result = loop monocs ths
   5.431      in
   5.432 -	(!changed, result)
   5.433 -    end	    
   5.434 +        (!changed, result)
   5.435 +    end
   5.436  
   5.437  datatype cthm = ComputeThm of term list * sort list * term
   5.438  
   5.439 -fun thm2cthm th = 
   5.440 +fun thm2cthm th =
   5.441      let
   5.442 -	val {hyps, prop, shyps, ...} = Thm.rep_thm th
   5.443 +        val {hyps, prop, shyps, ...} = Thm.rep_thm th
   5.444      in
   5.445 -	ComputeThm (hyps, shyps, prop)
   5.446 +        ComputeThm (hyps, shyps, prop)
   5.447      end
   5.448  
   5.449  val cthm_ord' = prod_ord (prod_ord (list_ord Term.term_ord) (list_ord Term.sort_ord)) Term.term_ord
   5.450 @@ -335,59 +337,59 @@
   5.451  fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
   5.452  
   5.453  structure CThmtab = TableFun (type key = cthm val ord = cthm_ord)
   5.454 -    
   5.455 +
   5.456  fun remove_duplicates ths =
   5.457      let
   5.458 -	val counter = ref 0 
   5.459 -	val tab = ref (CThmtab.empty : unit CThmtab.table)
   5.460 -	val thstab = ref (Inttab.empty : thm Inttab.table)
   5.461 -	fun update th = 
   5.462 -	    let
   5.463 -		val key = thm2cthm th
   5.464 -	    in
   5.465 -		case CThmtab.lookup (!tab) key of
   5.466 -		    NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
   5.467 -		  | _ => ()
   5.468 -	    end
   5.469 -	val _ = map update ths
   5.470 +        val counter = ref 0
   5.471 +        val tab = ref (CThmtab.empty : unit CThmtab.table)
   5.472 +        val thstab = ref (Inttab.empty : thm Inttab.table)
   5.473 +        fun update th =
   5.474 +            let
   5.475 +                val key = thm2cthm th
   5.476 +            in
   5.477 +                case CThmtab.lookup (!tab) key of
   5.478 +                    NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
   5.479 +                  | _ => ()
   5.480 +            end
   5.481 +        val _ = map update ths
   5.482      in
   5.483 -	map snd (Inttab.dest (!thstab))
   5.484 +        map snd (Inttab.dest (!thstab))
   5.485      end
   5.486 -    
   5.487 +
   5.488  
   5.489  fun make machine thy ths cs =
   5.490      let
   5.491 -	val ths = remove_duplicates ths
   5.492 -	val (monocs, ths) = fold_rev (fn th => 
   5.493 -				      fn (monocs, ths) => 
   5.494 -					 let val (m, t) = create_theorem th in 
   5.495 -					     (m@monocs, t::ths)
   5.496 -					 end)
   5.497 -				     ths (cs, [])
   5.498 -	val (_, ths) = add_monos thy monocs ths
   5.499 +        val ths = remove_duplicates ths
   5.500 +        val (monocs, ths) = fold_rev (fn th =>
   5.501 +                                      fn (monocs, ths) =>
   5.502 +                                         let val (m, t) = create_theorem th in
   5.503 +                                             (m@monocs, t::ths)
   5.504 +                                         end)
   5.505 +                                     ths (cs, [])
   5.506 +        val (_, ths) = add_monos thy monocs ths
   5.507    val computer = create_computer machine thy ths
   5.508      in
   5.509 -	PComputer (machine, Theory.check_thy thy, ref computer, ref ths)
   5.510 +        PComputer (machine, Theory.check_thy thy, ref computer, ref ths)
   5.511      end
   5.512  
   5.513 -fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs = 
   5.514 +fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs =
   5.515      let
   5.516 -	val thy = Theory.deref thyref
   5.517 -	val (changed, ths) = add_monos thy cs (!rths)
   5.518 +        val thy = Theory.deref thyref
   5.519 +        val (changed, ths) = add_monos thy cs (!rths)
   5.520      in
   5.521 -	if changed then 
   5.522 -	    (rcomputer := create_computer machine thy ths;
   5.523 -	     rths := ths;
   5.524 -	     true)
   5.525 -	else
   5.526 -	    false
   5.527 +        if changed then
   5.528 +            (rcomputer := create_computer machine thy ths;
   5.529 +             rths := ths;
   5.530 +             true)
   5.531 +        else
   5.532 +            false
   5.533      end
   5.534  
   5.535  fun rewrite (pc as PComputer (_, _, rcomputer, _)) cts =
   5.536      let
   5.537 -	val _ = map (fn ct => add_instances pc (Linker.collect_consts [term_of ct])) cts
   5.538 +        val _ = map (fn ct => add_instances pc (Linker.collect_consts [term_of ct])) cts
   5.539      in
   5.540 -	map (fn ct => Compute.rewrite (!rcomputer) ct) cts
   5.541 +        map (fn ct => Compute.rewrite (!rcomputer) ct) cts
   5.542      end
   5.543 -		 							      			    
   5.544 +
   5.545  end