1.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:25:31 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:26:09 2012 +0100
     1.3 @@ -14,25 +14,7 @@
     1.4    morphisms member Set
     1.5    unfolding set_def by auto
     1.6  
     1.7 -text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
     1.8 -
     1.9 -local_setup {* fn lthy =>
    1.10 -  let
    1.11 -    val quotients =
    1.12 -      {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
    1.13 -        equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
    1.14 -    val qty_full_name = @{type_name "set"}
    1.15 -
    1.16 -    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    1.17 -  in
    1.18 -    lthy
    1.19 -    |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.20 -        (fn phi =>
    1.21 -          Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
    1.22 -          Quotient_Info.update_abs_rep qty_full_name
    1.23 -            (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
    1.24 -  end
    1.25 -*}
    1.26 +setup_lifting type_definition_set[unfolded set_def]
    1.27  
    1.28  text {* Now, we can employ quotient_definition to lift definitions. *}
    1.29  
    1.30 @@ -51,5 +33,7 @@
    1.31  term "Lift_Set.insert"
    1.32  thm Lift_Set.insert_def
    1.33  
    1.34 +export_code empty insert in SML
    1.35 +
    1.36  end
    1.37