src/Pure/Isar/expression.ML
changeset 29019 8e7d6f959bd7
parent 29018 17538bdef546
child 29020 3e95d28114a1
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 05 16:41:36 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Dec 08 14:18:29 2008 +0100
     1.3 @@ -370,6 +370,7 @@
     1.4                Term.fold_aterms (fn Free (x, T) =>
     1.5                  if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
     1.6            in Term.list_all_free (rev rev_frees, t) end;
     1.7 +  (* FIXME consider closing in syntactic phase *)
     1.8  
     1.9          fun no_binds [] = []
    1.10            | no_binds _ = error "Illegal term bindings in context element";
    1.11 @@ -378,7 +379,7 @@
    1.12            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
    1.13              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
    1.14          | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
    1.15 -            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
    1.16 +            (a, (close_frees (#2 (LocalDefs.cert_def ctxt (close_frees t))), no_binds ps))))
    1.17          | e => e)
    1.18        end;
    1.19