# HG changeset patch
# User boehmes
# Date 1292404368 -3600
# Node ID b88cfc0f745628cd0e9d47c0ed671beb55a24c3e
# Parent  bb2fa5c13d1a5774bf9fcbe79376e100f8ccccb4
also show function definitions for higher-order free variables in Z3 models

diff -r bb2fa5c13d1a -r b88cfc0f7456 src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Wed Dec 15 10:12:48 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -290,6 +290,17 @@
 
 val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
 
+fun is_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true
+  | is_free_def _ = false
+
+fun defined tp =
+  try (pairself (fst o HOLogic.dest_eq)) tp
+  |> the_default false o Option.map (op aconv)
+
+fun add_free_defs free_cs defs =
+  let val (free_defs, defs') = List.partition is_free_def defs
+  in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end
+
 fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
   | is_const_def _ = false
 
@@ -302,6 +313,7 @@
   |> unfold_eqs
   |>> map swap_free
   |>> filter is_free_constraint
+  |-> add_free_defs
   |> frees_for_vars ctxt
   ||> filter is_const_def