# HG changeset patch
# User oheimb
# Date 906412408 -7200
# Node ID 982c710450c6ad016b1cd66a4a0e8214c68bf8a8
# Parent  7970832271cc5b1a4bd31f7c871dfa58ffb6b4bf
improved indentation

diff -r 7970832271cc -r 982c710450c6 src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Mon Sep 21 23:12:31 1998 +0200
+++ b/src/HOL/MiniML/Generalize.ML	Mon Sep 21 23:13:28 1998 +0200
@@ -64,7 +64,7 @@
 
 Goalw [gen_ML_def] "gen A t = gen_ML A t";
 by (induct_tac "t" 1);
-by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
+ by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 qed "gen_eq_gen_ML";