--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sat Sep 13 18:08:38 2014 +0200
@@ -250,9 +250,9 @@
end;
val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
- lthy
- |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
- ||> `Local_Theory.restore;
+ lthy
+ |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
+ ||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));