# HG changeset patch
# User wenzelm
# Date 1470407763 -7200
# Node ID fb63942e470eeceddb53b8fcd55dfade24b7e7ef
# Parent  4b40b8196dc7874e954650b8079f2fc8876c781d
tuned whitespace;

diff -r 4b40b8196dc7 -r fb63942e470e src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Aug 05 16:30:53 2016 +0200
+++ b/src/Pure/term.ML	Fri Aug 05 16:36:03 2016 +0200
@@ -181,12 +181,12 @@
   for resolution.*)
 type indexname = string * int;
 
-(* Types are classified by sorts. *)
+(*Types are classified by sorts.*)
 type class = string;
 type sort  = class list;
 type arity = string * sort list * sort;
 
-(* The sorts attached to TFrees and TVars specify the sort of that variable *)
+(*The sorts attached to TFrees and TVars specify the sort of that variable.*)
 datatype typ = Type  of string * typ list
              | TFree of string * sort
              | TVar  of indexname * sort;
@@ -293,15 +293,15 @@
   | dest_funT T = raise TYPE ("dest_funT", [T], []);
 
 
-(* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
+(*maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
 fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
   | binder_types _ = [];
 
-(* maps  [T1,...,Tn]--->T  to T*)
+(*maps  [T1,...,Tn]--->T  to T*)
 fun body_type (Type ("fun", [_, U])) = body_type U
   | body_type T = T;
 
-(* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
+(*maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)*)
 fun strip_type T = (binder_types T, body_type T);
 
 
@@ -361,11 +361,11 @@
       in ((a, T) :: a', t') end
   | strip_abs t = ([], t);
 
-(* maps  (x1,...,xn)t   to   t  *)
+(*maps  (x1,...,xn)t   to   t*)
 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   | strip_abs_body u  =  u;
 
-(* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
+(*maps  (x1,...,xn)t   to   [x1, ..., xn]*)
 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   | strip_abs_vars u  =  [] : (string*typ) list;
 
@@ -381,18 +381,18 @@
 in strip end;
 
 
-(* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
+(*maps   (f, [t1,...,tn])  to  f(t1,...,tn)*)
 val list_comb : term * term list -> term = Library.foldl (op $);
 
 
-(* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
+(*maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
 fun strip_comb u : term * term list =
     let fun stripc (f$t, ts) = stripc (f, t::ts)
         |   stripc  x =  x
     in  stripc(u,[])  end;
 
 
-(* maps   f(t1,...,tn)  to  f , which is never a combination *)
+(*maps   f(t1,...,tn)  to  f , which is never a combination*)
 fun head_of (f$t) = head_of f
   | head_of u = u;
 
@@ -580,11 +580,11 @@
 
 val propT : typ = Type ("prop",[]);
 
-(* maps  !!x1...xn. t   to   t  *)
+(*maps  !!x1...xn. t   to   t*)
 fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t
   | strip_all_body t = t;
 
-(* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
+(*maps  !!x1...xn. t   to   [x1, ..., xn]*)
 fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t
   | strip_all_vars t = [];
 
diff -r 4b40b8196dc7 -r fb63942e470e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 05 16:30:53 2016 +0200
+++ b/src/Pure/thm.ML	Fri Aug 05 16:36:03 2016 +0200
@@ -1319,7 +1319,7 @@
       prop = prop'})
   end;
 
-(* Replace all TFrees not fixed or in the hyps by new TVars *)
+(*Replace all TFrees not fixed or in the hyps by new TVars*)
 fun varifyT_global' fixed (Thm (der, {cert, maxidx, shyps, hyps, tpairs, prop, ...})) =
   let
     val tfrees = fold Term.add_tfrees hyps fixed;
@@ -1339,7 +1339,7 @@
 
 val varifyT_global = #2 o varifyT_global' [];
 
-(* Replace all TVars by TFrees that are often new *)
+(*Replace all TVars by TFrees that are often new*)
 fun legacy_freezeT (Thm (der, {cert, shyps, hyps, tpairs, prop, ...})) =
   let
     val prop1 = attach_tpairs tpairs prop;
@@ -1635,7 +1635,7 @@
      and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
      val cert = join_certificate2 (state, orule);
      val context = make_context [state, orule] opt_ctxt cert;
-     (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
+     (*Add new theorem with prop = '[| Bs; As |] ==> C' to thq*)
      fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
        let val normt = Envir.norm_term env;
            (*perform minimal copying here by examining env*)