src/HOL/Decision_Procs/Ferrack.thy
changeset 69266 7cc2d66a92a6
parent 69064 5840724b1d71
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 08 14:58:04 2018 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 08 15:49:56 2018 +0100
     1.3 @@ -2543,7 +2543,7 @@
     1.4      val vs = Term.add_frees t [];
     1.5      val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
     1.6    in (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
     1.7 -end;
     1.8 +end
     1.9  \<close>
    1.10  
    1.11  ML_file "ferrack_tac.ML"