# HG changeset patch
# User wenzelm
# Date 1709666445 -3600
# Node ID ece213b90d0f72076c40810c11020936c59bb57a
# Parent  b053bd598887b1a9206c31aa0a542cac01536a5b
tuned whitespace: avoid TABs;

diff -r b053bd598887 -r ece213b90d0f src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 05 20:20:34 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 05 20:20:45 2024 +0100
@@ -599,7 +599,7 @@
 
     val SOME {pre_bnf, absT_info = {abs_inverse, ...},
         fp_ctr_sugar = {ctr_defs, ctr_sugar = {ctrs = ctrs0, ...}, ...},
-		live_nesting_bnfs = live_nesting_bnfs, ...} =
+        live_nesting_bnfs = live_nesting_bnfs, ...} =
       fp_sugar_of ctxt fpT_name;
 
     val ctrs = map (mk_ctr fp_argTs) ctrs0;
@@ -611,7 +611,7 @@
       Variable.add_free_names ctxt goal []
       |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
         mk_cong_intro_ctr_or_friend_tac ctxt ctr_def
-		  ([pre_rel_def, abs_inverse] @ live_nesting_rel_eqs) cong_ctor_intro))
+          ([pre_rel_def, abs_inverse] @ live_nesting_rel_eqs) cong_ctor_intro))
       |> Thm.close_derivation \<^here>;
 
     val goals = map (mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong) ctrs;