src/Pure/goal.ML
changeset 50987 616789281413
parent 50974 55f8bd61b029
child 51110 ef0592498418
equal deleted inserted replaced
50986:c54ea7f5418f 50987:616789281413
   223         Drule.forall_intr_list fixes #>
   223         Drule.forall_intr_list fixes #>
   224         Thm.generalize (map #1 tfrees, []) 0 #>
   224         Thm.generalize (map #1 tfrees, []) 0 #>
   225         Thm.strip_shyps);
   225         Thm.strip_shyps);
   226     val local_result =
   226     val local_result =
   227       Thm.future global_result global_prop
   227       Thm.future global_result global_prop
       
   228       |> Thm.close_derivation
   228       |> Thm.instantiate (instT, [])
   229       |> Thm.instantiate (instT, [])
   229       |> Drule.forall_elim_list fixes
   230       |> Drule.forall_elim_list fixes
   230       |> fold (Thm.elim_implies o Thm.assume) assms;
   231       |> fold (Thm.elim_implies o Thm.assume) assms;
   231   in local_result end;
   232   in local_result end;
   232 
   233