src/Pure/Isar/expression.ML
changeset 29021 ce100fbc3c8e
parent 29020 3e95d28114a1
child 29022 54d3a31ca0f6
child 29033 721529248e31
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Dec 08 14:22:42 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Mon Dec 08 18:44:24 2008 +0100
     1.3 @@ -369,7 +369,7 @@
     1.4              val rev_frees =
     1.5                Term.fold_aterms (fn Free (x, T) =>
     1.6                  if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
     1.7 -          in Term.list_all_free (rev rev_frees, t) end;
     1.8 +          in Term.list_all_free (rev rev_frees, t) end; (* FIXME use fold Logic.all *)
     1.9    (* FIXME consider closing in syntactic phase *)
    1.10  
    1.11          fun no_binds [] = []
    1.12 @@ -379,7 +379,7 @@
    1.13            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
    1.14              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
    1.15          | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
    1.16 -            (a, (close_frees (#2 (LocalDefs.cert_def ctxt (close_frees t))), no_binds ps))))
    1.17 +            (a, (#2 (LocalDefs.cert_def ctxt (close_frees t)), no_binds ps))))
    1.18          | e => e)
    1.19        end;
    1.20  
    1.21 @@ -545,6 +545,7 @@
    1.22        NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
    1.23      val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
    1.24    in ((fixed, deps, elems'), (parms, spec, defs)) end;
    1.25 +  (* FIXME check if defs used somewhere *)
    1.26  
    1.27  in
    1.28  
    1.29 @@ -734,7 +735,7 @@
    1.30      let
    1.31        val defs' = map (fn (_, (def, _)) => def) defs
    1.32        val notes = map (fn (a, (def, _)) =>
    1.33 -        (a, [([assume (cterm_of thy def)], [])])) defs
    1.34 +        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs
    1.35      in
    1.36        (Notes (Thm.definitionK, notes), defns @ defs')
    1.37      end
    1.38 @@ -743,13 +744,12 @@
    1.39  fun gen_add_locale prep_decl
    1.40      bname predicate_name raw_imprt raw_body thy =
    1.41    let
    1.42 -    val thy_ctxt = ProofContext.init thy;
    1.43      val name = Sign.full_bname thy bname;
    1.44      val _ = NewLocale.test_locale thy name andalso
    1.45        error ("Duplicate definition of locale " ^ quote name);
    1.46  
    1.47 -    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
    1.48 -      prep_decl raw_imprt raw_body thy_ctxt;
    1.49 +    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), _)) =
    1.50 +      prep_decl raw_imprt raw_body (ProofContext.init thy);
    1.51      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
    1.52        define_preds predicate_name text thy;
    1.53  
    1.54 @@ -776,7 +776,7 @@
    1.55  
    1.56      val loc_ctxt = thy' |>
    1.57        NewLocale.register_locale bname (extraTs, params)
    1.58 -        (asm, map prop_of defs) ([], [])
    1.59 +        (asm, defns) ([], [])
    1.60          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
    1.61        NewLocale.init name
    1.62    in (name, loc_ctxt) end;