src/Pure/Isar/proof.ML

 (* refine via sub-proof *)
 
 local
 
 fun refine_tac rule =
-  Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) =>
-    if can Logic.unprotect (Logic.strip_assums_concl goal) then
-      Tactic.etac Drule.protectI i
-    else all_tac));
+  Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW
+    (Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) =>
+      if can Logic.unprotect (Logic.strip_assums_concl goal) then
+        Tactic.etac Drule.protectI i
+      else all_tac)));
 
 fun refine_goal print_rule inner raw_rule state =
   let val (outer, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state in
     raw_rule
     |> ProofContext.goal_exports inner outer

     val _ = assert_forward state;
     val thy = theory_of state;
     val ctxt = context_of state;
 
     val rhs = prep_term ctxt raw_rhs;
-    val T = Term.fastype_of rhs;
-    val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats;
-    val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
-
+    val pats = prep_pats (Term.fastype_of rhs) (ProofContext.declare_term rhs ctxt) raw_pats;
+    val eq = ProofContext.mk_def ctxt (x, rhs);
     val name = if raw_name = "" then Thm.def_name x else raw_name;
     val atts = map (prep_att thy) raw_atts;
   in
     state
     |> fix [([x], NONE)]
     |> match_bind_i [(pats, rhs)]
-    |> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
+    |> assm_i ProofContext.export_def [((name, atts), [(eq, ([], []))])]
   end;
 
 in
 
 val def = gen_def fix Attrib.local_attribute ProofContext.read_term ProofContext.read_term_pats;