# HG changeset patch
# User wenzelm
# Date 1442930299 -7200
# Node ID 76148d288b2ec585667fdf4a5843588d1ab49537
# Parent  077b88f9ec1653b76624d8f7d0f0cf91128dab61
tuned whitespace;

diff -r 077b88f9ec16 -r 76148d288b2e src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Sep 22 14:32:23 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Tue Sep 22 15:58:19 2015 +0200
@@ -132,14 +132,14 @@
       |> Local_Theory.background_theory_result
         (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
           Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
-       
+
     fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts
       | fold_type_constr _ _ = I;
-    
+
     val A_consts = fold_aterms (fn Const const => insert (op =) (Theory.DConst const) | _ => I) A [];
-    val A_types = fold_types (fold_type_constr (insert (op =) o Theory.DType)) A []
+    val A_types = fold_types (fold_type_constr (insert (op =) o Theory.DType)) A [];
     val typedef_deps = A_consts @ A_types;
-    
+
     val newT_dep = Theory.DType (dest_Type newT);
 
     val ((axiom_name, axiom), axiom_lthy) = consts_lthy
diff -r 077b88f9ec16 -r 76148d288b2e src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Tue Sep 22 14:32:23 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML	Tue Sep 22 15:58:19 2015 +0200
@@ -56,7 +56,7 @@
 
 fun basic_typedecl final (b, n, mx) lthy =
   let
-    fun make_final lthy = 
+    fun make_final lthy =
       let
         val tfree_names = Name.invent (Variable.names_of lthy) Name.aT n
         val tfrees = map (fn name => (name, [])) tfree_names
@@ -134,4 +134,3 @@
   #> Local_Theory.exit_result_global (K I);
 
 end;
-
diff -r 077b88f9ec16 -r 76148d288b2e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Sep 22 14:32:23 2015 +0200
+++ b/src/Pure/axclass.ML	Tue Sep 22 15:58:19 2015 +0200
@@ -614,7 +614,7 @@
     thy
     |> Sign.primitive_class (bclass, super)
     |> classrel_axiomatization (map (fn c => (class, c)) super)
-    |> Theory.add_deps_global "" (Theory.DConst (class_const class)) 
+    |> Theory.add_deps_global "" (Theory.DConst (class_const class))
       (map (Theory.DConst o class_const) super)
   end;
 
diff -r 077b88f9ec16 -r 76148d288b2e src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 22 14:32:23 2015 +0200
+++ b/src/Pure/theory.ML	Tue Sep 22 15:58:19 2015 +0200
@@ -23,7 +23,7 @@
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
-  datatype dep = DConst of string * typ | DType of string * typ list 
+  datatype dep = DConst of string * typ | DType of string * typ list
   val add_deps: Proof.context -> string -> dep -> dep list -> theory -> theory
   val add_deps_global: string -> dep -> dep list -> theory -> theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
@@ -212,7 +212,7 @@
 
 (* dependencies *)
 
-datatype dep = DConst of string * typ | DType of string * typ list 
+datatype dep = DConst of string * typ | DType of string * typ list
 
 fun name_of_dep (DConst (s, _)) = s
   | name_of_dep (DType (s, _)) = s
@@ -224,13 +224,13 @@
     fun prep (DConst const) =
       let val Const (c, T) = Sign.no_vars ctxt (Const const)
       in (Defs.NConst c, Consts.typargs consts (c, Logic.varifyT_global T)) end
-    | prep (DType typ) = 
+    | prep (DType typ) =
       let val Type (c, T) = Type.no_tvars (Type typ)
       in (Defs.NType c, map Logic.varifyT_global T) end;
     fun fold_dep_tfree f (DConst (_, T)) = fold_atyps (fn TFree v => f v | _ => I) T
       | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts
     val lhs_vars = fold_dep_tfree (insert (op =)) lhs [];
-    val rhs_extras = fold (fold_dep_tfree 
+    val rhs_extras = fold (fold_dep_tfree
       (fn v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
     val _ =
       if null rhs_extras then ()