# HG changeset patch
# User haftmann
# Date 1267017594 -3600
# Node ID 6c92eb394e3cef3831a9cf6eb7c0e6ad686bc6b2
# Parent  997a23ae1aa053ad572917e83d5e760e4faba2e9
tuned whitespace

diff -r 997a23ae1aa0 -r 6c92eb394e3c src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Feb 24 14:19:54 2010 +0100
+++ b/src/Tools/nbe.ML	Wed Feb 24 14:19:54 2010 +0100
@@ -164,6 +164,7 @@
   | same _ _ = false
 and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys);
 
+
 (* constructor functions *)
 
 fun abss n f = Abs ((n, f), []);
@@ -213,6 +214,7 @@
         |> suffix "\n"
       end;
 
+
 (* nbe specific syntax and sandbox communication *)
 
 val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
@@ -255,6 +257,7 @@
 
 open Basic_Code_Thingol;
 
+
 (* code generation *)
 
 fun assemble_eqnss idx_of deps eqnss =
@@ -330,7 +333,7 @@
         val match_cont = if is_eval then NONE else SOME default_rhs;
         val assemble_arg = assemble_iterm
           (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
-        val assemble_rhs = assemble_iterm assemble_constapp match_cont ;
+        val assemble_rhs = assemble_iterm assemble_constapp match_cont;
         val (samepairs, args') = subst_nonlin_vars args;
         val s_args = map assemble_arg args';
         val s_rhs = if null samepairs then assemble_rhs rhs
@@ -357,6 +360,7 @@
     val deps_vars = ml_list (map (nbe_fun 0) deps);
   in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
 
+
 (* code compilation *)
 
 fun compile_eqnss _ gr raw_deps [] = []
@@ -457,6 +461,7 @@
     |> (fn t => apps t (rev dict_frees))
   end;
 
+
 (* reification *)
 
 fun typ_of_itype program vs (ityco `%% itys) =
@@ -480,9 +485,9 @@
       | is_dict (DFree _) = true
       | is_dict _ = false;
     fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
-         of Code_Thingol.Fun (c, _) => c
-          | Code_Thingol.Datatypecons (c, _) => c
-          | Code_Thingol.Classparam (c, _) => c);
+     of Code_Thingol.Fun (c, _) => c
+      | Code_Thingol.Datatypecons (c, _) => c
+      | Code_Thingol.Classparam (c, _) => c);
     fun of_apps bounds (t, ts) =
       fold_map (of_univ bounds) ts
       #>> (fn ts' => list_comb (t, rev ts'))
@@ -503,6 +508,7 @@
           |-> (fn t' => pair (Term.Abs ("u", dummyT, t')))
   in of_univ 0 t 0 |> fst end;
 
+
 (* function store *)
 
 structure Nbe_Functions = Code_Data
@@ -511,6 +517,7 @@
   val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
 );
 
+
 (* compilation, evaluation and reification *)
 
 fun compile_eval thy naming program vs_t deps =
@@ -524,6 +531,7 @@
     |> term_of_univ thy program idx_tab
   end;
 
+
 (* evaluation with type reconstruction *)
 
 fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
@@ -593,6 +601,7 @@
 
 fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (normalize thy)));
 
+
 (* evaluation command *)
 
 fun norm_print_term ctxt modes t =